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