Bob is blue. Bob is cold. Bob is green. Bob is quiet. Bob is red. Dave is young. Erin is blue. Erin is green. Erin is smart. Erin is young. All smart, blue things are young. Young things are cold. If something is young then it is smart. If something is blue and quiet then it is cold. If something is quiet and blue then it is cold. Cold, green things are red. All quiet, smart things are young. Red, green things are quiet.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is young.
("Erin" "is" "young" "+")
All smart, blue things are young.
((("something" "is" "smart" "+") ("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
Young things are cold.
((("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
If something is young then it is smart.
((("something" "is" "young" "+")) -> ("something" "is" "smart" "+"))
If something is blue and quiet then it is cold.
((("something" "is" "blue" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
If something is quiet and blue then it is cold.
((("something" "is" "quiet" "+") ("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
Cold, green things are red.
((("something" "is" "cold" "+") ("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
All quiet, smart things are young.
((("something" "is" "quiet" "+") ("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
Red, green things are quiet.
((("something" "is" "red" "+") ("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
Bob is red.
True
1
proof
[(triple5 OR ((triple2 triple3) -> rule6) OR ((((triple1 triple4) -> rule4) triple3) -> rule6) OR ((((triple4 triple1) -> rule5) triple3) -> rule6))]
("Bob" "is" "red" "+")
triple5
((triple2 triple3) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((((triple1 triple4) -> (rule4 % int2)) triple3) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
((((triple4 triple1) -> (rule5 % int2)) triple3) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is not red.
False
1
inv-proof
[(triple5 OR ((triple2 triple3) -> rule6) OR ((((triple1 triple4) -> rule4) triple3) -> rule6) OR ((((triple4 triple1) -> rule5) triple3) -> rule6))]
("Bob" "is" "red" "-")
triple5
((triple2 triple3) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((((triple1 triple4) -> (rule4 % int2)) triple3) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
((((triple4 triple1) -> (rule5 % int2)) triple3) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Dave is smart.
True
2
proof
[(((triple6) -> rule3))]
("Dave" "is" "smart" "+")
((triple6) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Erin is not cold.
False
2
inv-proof
[(((triple10) -> rule2) OR ((((triple9 triple7) -> rule1)) -> rule2))]
("Erin" "is" "cold" "-")
((triple10) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((((triple9 triple7) -> (rule1 % int2))) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is red.
True
4
proof
[(((((triple10) -> rule2) triple8) -> rule6) OR ((((((triple9 triple7) -> rule1)) -> rule2) triple8) -> rule6))]
("Erin" "is" "red" "+")
((((triple10) -> (rule2 % int2)) triple8) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
((((((triple9 triple7) -> (rule1 % int3))) -> (rule2 % int2)) triple8) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is not red.
False
4
inv-proof
[(((((triple10) -> rule2) triple8) -> rule6) OR ((((((triple9 triple7) -> rule1)) -> rule2) triple8) -> rule6))]
("Erin" "is" "red" "-")
((((triple10) -> (rule2 % int2)) triple8) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
((((((triple9 triple7) -> (rule1 % int3))) -> (rule2 % int2)) triple8) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is quiet.
True
6
proof
[(((((((triple10) -> rule2) triple8) -> rule6) triple8) -> rule8) OR ((((((((triple9 triple7) -> rule1)) -> rule2) triple8) -> rule6) triple8) -> rule8))]
("Erin" "is" "quiet" "+")
((((((triple10) -> (rule2 % int3)) triple8) -> (rule6 % int2)) triple8) -> (rule8 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
((((((((triple9 triple7) -> (rule1 % int4))) -> (rule2 % int3)) triple8) -> (rule6 % int2)) triple8) -> (rule8 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
int4
Erin is not quiet.
False
6
inv-proof
[(((((((triple10) -> rule2) triple8) -> rule6) triple8) -> rule8) OR ((((((((triple9 triple7) -> rule1)) -> rule2) triple8) -> rule6) triple8) -> rule8))]
("Erin" "is" "quiet" "-")
((((((triple10) -> (rule2 % int3)) triple8) -> (rule6 % int2)) triple8) -> (rule8 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
((((((((triple9 triple7) -> (rule1 % int4))) -> (rule2 % int3)) triple8) -> (rule6 % int2)) triple8) -> (rule8 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
int4
Dave is not red.
Unknown
inv-rconc
[@1: Dave is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "red" "-")
Bob is smart.
Unknown
rconc
[@2: Bob is smart.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Bob" "is" "smart" "+")
Bob is not young.
Unknown
inv-rconc
[@3: Bob is young.[CWA. Example of deepest failure = (rule1 <- rule3 <- rule7 <- FAIL)]]
("Bob" "is" "young" "-")
Dave is quiet.
Unknown
rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Dave" "is" "quiet" "+")
Dave is not blue.
Unknown
inv-random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "-")
Dave is green.
Unknown
random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "+")
@0: Bob is blue.[(triple1)] Bob is cold.[(triple2 OR ((triple1 triple4) -> rule4) OR ((triple4 triple1) -> rule5) OR ((triple1 ((triple5 triple3) -> rule8)) -> rule4) OR ((((triple5 triple3) -> rule8) triple1) -> rule5))] Bob is green.[(triple3)] Bob is quiet.[(triple4 OR ((triple5 triple3) -> rule8) OR ((((triple2 triple3) -> rule6) triple3) -> rule8))] Bob is red.[(triple5 OR ((triple2 triple3) -> rule6) OR ((((triple1 triple4) -> rule4) triple3) -> rule6) OR ((((triple4 triple1) -> rule5) triple3) -> rule6))] Dave is young.[(triple6)] Erin is blue.[(triple7)] Erin is green.[(triple8)] Erin is smart.[(triple9 OR ((triple10) -> rule3))] Erin is young.[(triple10 OR ((triple9 triple7) -> rule1))] @1: Dave is cold.[(((triple6) -> rule2))] Dave is smart.[(((triple6) -> rule3))] Erin is cold.[(((triple10) -> rule2) OR ((((triple9 triple7) -> rule1)) -> rule2))] @2: Erin is red.[(((((triple10) -> rule2) triple8) -> rule6) OR ((((((triple9 triple7) -> rule1)) -> rule2) triple8) -> rule6))] @3: Erin is quiet.[(((((((triple10) -> rule2) triple8) -> rule6) triple8) -> rule8) OR ((((((((triple9 triple7) -> rule1)) -> rule2) triple8) -> rule6) triple8) -> rule8))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
((triple1 triple4) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((triple4 triple1) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((triple1 ((triple5 triple3) -> (rule8 % int2))) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
((((triple5 triple3) -> (rule8 % int2)) triple1) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
((triple5 triple3) -> (rule8 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((triple2 triple3) -> (rule6 % int2)) triple3) -> (rule8 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
triple5
((triple2 triple3) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((((triple1 triple4) -> (rule4 % int2)) triple3) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
((((triple4 triple1) -> (rule5 % int2)) triple3) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
triple6
Erin is blue.
("Erin" "is" "blue" "+")
triple7
Erin is green.
("Erin" "is" "green" "+")
triple8
Erin is smart.
("Erin" "is" "smart" "+")
triple9
((triple10) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
triple10
((triple9 triple7) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
((triple6) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple6) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
((triple10) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((((triple9 triple7) -> (rule1 % int2))) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
((((triple10) -> (rule2 % int2)) triple8) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
((((((triple9 triple7) -> (rule1 % int3))) -> (rule2 % int2)) triple8) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
((((((triple10) -> (rule2 % int3)) triple8) -> (rule6 % int2)) triple8) -> (rule8 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
((((((((triple9 triple7) -> (rule1 % int4))) -> (rule2 % int3)) triple8) -> (rule6 % int2)) triple8) -> (rule8 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
int4