Anne is blue. Bob is white. Dave is red. Dave is rough. Harry is blue. Harry is not rough. Harry is smart. If someone is green then they are blue. If someone is white and not red then they are blue. All blue people are white. If someone is nice and red then they are white. If someone is green then they are white. If Harry is blue and Harry is rough then Harry is green. All white people are green. All rough people are nice. Blue people are smart.
Anne is blue.
("Anne" "is" "blue" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is not rough.
("Harry" "is" "rough" "-")
Harry is smart.
("Harry" "is" "smart" "+")
If someone is green then they are blue.
((("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
If someone is white and not red then they are blue.
((("someone" "is" "white" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "blue" "+"))
All blue people are white.
((("someone" "is" "blue" "+")) -> ("someone" "is" "white" "+"))
If someone is nice and red then they are white.
((("someone" "is" "nice" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "white" "+"))
If someone is green then they are white.
((("someone" "is" "green" "+")) -> ("someone" "is" "white" "+"))
If Harry is blue and Harry is rough then Harry is green.
((("Harry" "is" "blue" "+") ("Harry" "is" "rough" "+")) -> ("Harry" "is" "green" "+"))
All white people are green.
((("someone" "is" "white" "+")) -> ("someone" "is" "green" "+"))
All rough people are nice.
((("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
Blue people are smart.
((("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "+"))
Anne is blue.
True
1
proof
[(triple1)]
("Anne" "is" "blue" "+")
triple1
Anne is not blue.
False
1
inv-proof
[(triple1)]
("Anne" "is" "blue" "-")
triple1
Anne is white.
True
2
proof
[(((triple1) -> rule3))]
("Anne" "is" "white" "+")
((triple1) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is not white.
False
2
inv-proof
[(((triple1) -> rule3))]
("Anne" "is" "white" "-")
((triple1) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Dave is white.
True
4
proof
[(((((triple4) -> rule8) triple3) -> rule4))]
("Dave" "is" "white" "+")
((((triple4) -> (rule8 % int2)) triple3) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is not white.
False
4
inv-proof
[(((((triple4) -> rule8) triple3) -> rule4))]
("Dave" "is" "white" "-")
((((triple4) -> (rule8 % int2)) triple3) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is green.
True
5
proof
[(((((((triple4) -> rule8) triple3) -> rule4)) -> rule7))]
("Dave" "is" "green" "+")
((((((triple4) -> (rule8 % int3)) triple3) -> (rule4 % int2))) -> (rule7 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Bob is not smart.
False
4
inv-proof
[(((((((triple2) -> rule7)) -> rule1)) -> rule9))]
("Bob" "is" "smart" "-")
((((((triple2) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule9 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Dave is blue.
True
6
proof
[(((((((((triple4) -> rule8) triple3) -> rule4)) -> rule7)) -> rule1))]
("Dave" "is" "blue" "+")
((((((((triple4) -> (rule8 % int4)) triple3) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
Dave is not blue.
False
6
inv-proof
[(((((((((triple4) -> rule8) triple3) -> rule4)) -> rule7)) -> rule1))]
("Dave" "is" "blue" "-")
((((((((triple4) -> (rule8 % int4)) triple3) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
Dave is smart.
True
7
proof
[(((((((((((triple4) -> rule8) triple3) -> rule4)) -> rule7)) -> rule1)) -> rule9))]
("Dave" "is" "smart" "+")
((((((((((triple4) -> (rule8 % int5)) triple3) -> (rule4 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule9 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
Dave is nice.
("Dave" "is" "nice" "+")
int5
Dave is not smart.
False
7
inv-proof
[(((((((((((triple4) -> rule8) triple3) -> rule4)) -> rule7)) -> rule1)) -> rule9))]
("Dave" "is" "smart" "-")
((((((((((triple4) -> (rule8 % int5)) triple3) -> (rule4 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule9 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
Dave is nice.
("Dave" "is" "nice" "+")
int5
Anne is not nice.
Unknown
inv-rconc
[@1: Anne is nice.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Anne" "is" "nice" "-")
Harry is nice.
Unknown
rconc
[@1: Harry is nice.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Harry" "is" "nice" "+")
Bob is not nice.
Unknown
inv-rconc
[@1: Bob is nice.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Bob" "is" "nice" "-")
Anne is rough.
Unknown
random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "+")
Anne is not red.
Unknown
inv-random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
Harry is not red.
Unknown
inv-random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
@0: Anne is blue.[(triple1)] Bob is white.[(triple2)] Dave is red.[(triple3)] Dave is rough.[(triple4)] Harry is blue.[(triple5)] Harry is not rough.[(triple6)] Harry is smart.[(triple7 OR ((triple5) -> rule9))] @1: Anne is smart.[(((triple1) -> rule9))] Anne is white.[(((triple1) -> rule3))] Bob is green.[(((triple2) -> rule7))] Dave is nice.[(((triple4) -> rule8))] Harry is white.[(((triple5) -> rule3))] @2: Anne is green.[(((((triple1) -> rule3)) -> rule7))] Bob is blue.[(((((triple2) -> rule7)) -> rule1))] Dave is white.[(((((triple4) -> rule8) triple3) -> rule4))] Harry is green.[(((((triple5) -> rule3)) -> rule7))] @3: Bob is smart.[(((((((triple2) -> rule7)) -> rule1)) -> rule9))] Dave is green.[(((((((triple4) -> rule8) triple3) -> rule4)) -> rule7))] @4: Dave is blue.[(((((((((triple4) -> rule8) triple3) -> rule4)) -> rule7)) -> rule1))] @5: Dave is smart.[(((((((((((triple4) -> rule8) triple3) -> rule4)) -> rule7)) -> rule1)) -> rule9))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Bob is white.
("Bob" "is" "white" "+")
triple2
Dave is red.
("Dave" "is" "red" "+")
triple3
Dave is rough.
("Dave" "is" "rough" "+")
triple4
Harry is blue.
("Harry" "is" "blue" "+")
triple5
Harry is not rough.
("Harry" "is" "rough" "-")
triple6
Harry is smart.
("Harry" "is" "smart" "+")
triple7
((triple5) -> (rule9 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule9 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
((triple1) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
((triple2) -> (rule7 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((triple4) -> (rule8 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple5) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
((((triple1) -> (rule3 % int2))) -> (rule7 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
((((triple2) -> (rule7 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
((((triple4) -> (rule8 % int2)) triple3) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
((((triple5) -> (rule3 % int2))) -> (rule7 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
((((((triple2) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule9 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
((((((triple4) -> (rule8 % int3)) triple3) -> (rule4 % int2))) -> (rule7 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
((((((((triple4) -> (rule8 % int4)) triple3) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
Dave is smart.
("Dave" "is" "smart" "+")
((((((((((triple4) -> (rule8 % int5)) triple3) -> (rule4 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule9 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
Dave is nice.
("Dave" "is" "nice" "+")
int5