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