Bob is cold. Bob is rough. Bob is young. Charlie is cold. Erin is red. Erin is rough. Erin is white. If someone is furry and cold then they are blue. If someone is rough then they are red. All young, red people are furry. All white, young people are blue. All white people are furry. All white, furry people are cold. All furry, young people are white. If someone is young then they are furry.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is white.
("Erin" "is" "white" "+")
If someone is furry and cold then they are blue.
((("someone" "is" "furry" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
If someone is rough then they are red.
((("someone" "is" "rough" "+")) -> ("someone" "is" "red" "+"))
All young, red people are furry.
((("someone" "is" "young" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "furry" "+"))
All white, young people are blue.
((("someone" "is" "white" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "blue" "+"))
All white people are furry.
((("someone" "is" "white" "+")) -> ("someone" "is" "furry" "+"))
All white, furry people are cold.
((("someone" "is" "white" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "cold" "+"))
All furry, young people are white.
((("someone" "is" "furry" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "white" "+"))
If someone is young then they are furry.
((("someone" "is" "young" "+")) -> ("someone" "is" "furry" "+"))
Bob is young.
True
1
proof
[(triple3)]
("Bob" "is" "young" "+")
triple3
Charlie is not cold.
False
1
inv-proof
[(triple4)]
("Charlie" "is" "cold" "-")
triple4
Bob is furry.
True
2
proof
[(((triple3) -> rule8) OR ((triple3 ((triple2) -> rule2)) -> rule3))]
("Bob" "is" "furry" "+")
((triple3) -> (rule8 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((triple3 ((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is not red.
False
2
inv-proof
[(((triple2) -> rule2))]
("Bob" "is" "red" "-")
((triple2) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
True
4
proof
[(((((triple3) -> rule8) triple3) -> rule7) OR ((((triple3 ((triple2) -> rule2)) -> rule3) triple3) -> rule7))]
("Bob" "is" "white" "+")
((((triple3) -> (rule8 % int2)) triple3) -> (rule7 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((((triple3 ((triple2) -> (rule2 % int3))) -> (rule3 % int2)) triple3) -> (rule7 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Erin is not cold.
False
4
inv-proof
[(((triple7 ((triple7) -> rule5)) -> rule6))]
("Erin" "is" "cold" "-")
((triple7 ((triple7) -> (rule5 % int2))) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is blue.
True
7
proof
[(((((triple7) -> rule5) ((triple7 ((triple7) -> rule5)) -> rule6)) -> rule1))]
("Erin" "is" "blue" "+")
((((triple7) -> (rule5 % int3)) ((triple7 ((triple7) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is not blue.
False
7
inv-proof
[(((((triple7) -> rule5) ((triple7 ((triple7) -> rule5)) -> rule6)) -> rule1))]
("Erin" "is" "blue" "-")
((((triple7) -> (rule5 % int3)) ((triple7 ((triple7) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Charlie is not white.
Unknown
inv-rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Charlie" "is" "white" "-")
Charlie is furry.
Unknown
rconc
[@2: Charlie is furry.[CWA. Example of deepest failure = (rule5 <- rule7 <- FAIL)]]
("Charlie" "is" "furry" "+")
Charlie is not red.
Unknown
inv-rconc
[@1: Charlie is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "red" "-")
Charlie is blue.
Unknown
rconc
[@3: Charlie is blue.[CWA. Example of deepest failure = (rule1 <- rule5 <- rule7 <- FAIL)]]
("Charlie" "is" "blue" "+")
Erin is not young.
Unknown
inv-random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "-")
Charlie is young.
Unknown
random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "+")
@0: Bob is cold.[(triple1 OR ((((((triple3) -> rule8) triple3) -> rule7) ((triple3) -> rule8)) -> rule6) OR ((((((triple3) -> rule8) triple3) -> rule7) ((triple3 ((triple2) -> rule2)) -> rule3)) -> rule6) OR ((((((triple3 ((triple2) -> rule2)) -> rule3) triple3) -> rule7) ((triple3) -> rule8)) -> rule6) OR ((((((triple3 ((triple2) -> rule2)) -> rule3) triple3) -> rule7) ((triple3 ((triple2) -> rule2)) -> rule3)) -> rule6))] Bob is rough.[(triple2)] Bob is young.[(triple3)] Charlie is cold.[(triple4)] Erin is red.[(triple5 OR ((triple6) -> rule2))] Erin is rough.[(triple6)] Erin is white.[(triple7)] @1: Bob is furry.[(((triple3) -> rule8) OR ((triple3 ((triple2) -> rule2)) -> rule3))] Bob is red.[(((triple2) -> rule2))] Erin is furry.[(((triple7) -> rule5))] @2: Bob is blue.[(((((triple3) -> rule8) triple1) -> rule1) OR ((((triple3 ((triple2) -> rule2)) -> rule3) triple1) -> rule1) OR ((((((triple3) -> rule8) triple3) -> rule7) triple3) -> rule4) OR ((((((triple3 ((triple2) -> rule2)) -> rule3) triple3) -> rule7) triple3) -> rule4) OR ((((triple3) -> rule8) ((((((triple3) -> rule8) triple3) -> rule7) ((triple3) -> rule8)) -> rule6)) -> rule1) OR ((((triple3) -> rule8) ((((((triple3) -> rule8) triple3) -> rule7) ((triple3 ((triple2) -> rule2)) -> rule3)) -> rule6)) -> rule1) OR ((((triple3 ((triple2) -> rule2)) -> rule3) ((((((triple3) -> rule8) triple3) -> rule7) ((triple3) -> rule8)) -> rule6)) -> rule1) OR ((((triple3 ((triple2) -> rule2)) -> rule3) ((((((triple3) -> rule8) triple3) -> rule7) ((triple3 ((triple2) -> rule2)) -> rule3)) -> rule6)) -> rule1) OR ((((triple3) -> rule8) ((((((triple3 ((triple2) -> rule2)) -> rule3) triple3) -> rule7) ((triple3) -> rule8)) -> rule6)) -> rule1) OR ((((triple3) -> rule8) ((((((triple3 ((triple2) -> rule2)) -> rule3) triple3) -> rule7) ((triple3 ((triple2) -> rule2)) -> rule3)) -> rule6)) -> rule1) OR ((((triple3 ((triple2) -> rule2)) -> rule3) ((((((triple3 ((triple2) -> rule2)) -> rule3) triple3) -> rule7) ((triple3) -> rule8)) -> rule6)) -> rule1) OR ((((triple3 ((triple2) -> rule2)) -> rule3) ((((((triple3 ((triple2) -> rule2)) -> rule3) triple3) -> rule7) ((triple3 ((triple2) -> rule2)) -> rule3)) -> rule6)) -> rule1))] Bob is white.[(((((triple3) -> rule8) triple3) -> rule7) OR ((((triple3 ((triple2) -> rule2)) -> rule3) triple3) -> rule7))] Erin is cold.[(((triple7 ((triple7) -> rule5)) -> rule6))] @3: Erin is blue.[(((((triple7) -> rule5) ((triple7 ((triple7) -> rule5)) -> rule6)) -> rule1))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
((((((triple3) -> (rule8 % int3)) triple3) -> (rule7 % int2)) ((triple3) -> (rule8 % int3))) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
((((((triple3) -> (rule8 % int4)) triple3) -> (rule7 % int3)) ((triple3 ((triple2) -> (rule2 % int2))) -> (rule3 % int4))) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
int4
((((((triple3 ((triple2) -> (rule2 % int4))) -> (rule3 % int3)) triple3) -> (rule7 % int2)) ((triple3) -> (rule8 % int3))) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
int4
((((((triple3 ((triple2) -> (rule2 % int4))) -> (rule3 % int3)) triple3) -> (rule7 % int2)) ((triple3 ((triple2) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
int4
Bob is rough.
("Bob" "is" "rough" "+")
triple2
Bob is young.
("Bob" "is" "young" "+")
triple3
Charlie is cold.
("Charlie" "is" "cold" "+")
triple4
Erin is red.
("Erin" "is" "red" "+")
triple5
((triple6) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
triple6
Erin is white.
("Erin" "is" "white" "+")
triple7
Bob is furry.
("Bob" "is" "furry" "+")
((triple3) -> (rule8 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((triple3 ((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
((triple2) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((triple7) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((((triple3) -> (rule8 % int2)) triple1) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((((triple3 ((triple2) -> (rule2 % int3))) -> (rule3 % int2)) triple1) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
((((((triple3) -> (rule8 % int3)) triple3) -> (rule7 % int2)) triple3) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
((((((triple3 ((triple2) -> (rule2 % int4))) -> (rule3 % int3)) triple3) -> (rule7 % int2)) triple3) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
int4
((((triple3) -> (rule8 % int4)) ((((((triple3) -> (rule8 % int4)) triple3) -> (rule7 % int3)) ((triple3) -> (rule8 % int4))) -> (rule6 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
int4
((((triple3) -> (rule8 % int5)) ((((((triple3) -> (rule8 % int5)) triple3) -> (rule7 % int4)) ((triple3 ((triple2) -> (rule2 % int3))) -> (rule3 % int5))) -> (rule6 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Bob is furry.
("Bob" "is" "furry" "+")
int5
((((triple3 ((triple2) -> (rule2 % int5))) -> (rule3 % int4)) ((((((triple3) -> (rule8 % int4)) triple3) -> (rule7 % int3)) ((triple3) -> (rule8 % int4))) -> (rule6 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
int4
Bob is red.
("Bob" "is" "red" "+")
int5
((((triple3 ((triple2) -> (rule2 % int5))) -> (rule3 % int4)) ((((((triple3) -> (rule8 % int4)) triple3) -> (rule7 % int3)) ((triple3 ((triple2) -> (rule2 % int5))) -> (rule3 % int4))) -> (rule6 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
int4
Bob is red.
("Bob" "is" "red" "+")
int5
((((triple3) -> (rule8 % int5)) ((((((triple3 ((triple2) -> (rule2 % int4))) -> (rule3 % int5)) triple3) -> (rule7 % int3)) ((triple3) -> (rule8 % int5))) -> (rule6 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
int4
Bob is furry.
("Bob" "is" "furry" "+")
int5
((((triple3) -> (rule8 % int5)) ((((((triple3 ((triple2) -> (rule2 % int4))) -> (rule3 % int5)) triple3) -> (rule7 % int3)) ((triple3 ((triple2) -> (rule2 % int4))) -> (rule3 % int5))) -> (rule6 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
int4
Bob is furry.
("Bob" "is" "furry" "+")
int5
((((triple3 ((triple2) -> (rule2 % int5))) -> (rule3 % int4)) ((((((triple3 ((triple2) -> (rule2 % int5))) -> (rule3 % int4)) triple3) -> (rule7 % int3)) ((triple3) -> (rule8 % int4))) -> (rule6 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
int4
Bob is red.
("Bob" "is" "red" "+")
int5
((((triple3 ((triple2) -> (rule2 % int5))) -> (rule3 % int4)) ((((((triple3 ((triple2) -> (rule2 % int5))) -> (rule3 % int4)) triple3) -> (rule7 % int3)) ((triple3 ((triple2) -> (rule2 % int5))) -> (rule3 % int4))) -> (rule6 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
int4
Bob is red.
("Bob" "is" "red" "+")
int5
Bob is white.
("Bob" "is" "white" "+")
((((triple3) -> (rule8 % int2)) triple3) -> (rule7 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((((triple3 ((triple2) -> (rule2 % int3))) -> (rule3 % int2)) triple3) -> (rule7 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
((triple7 ((triple7) -> (rule5 % int2))) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
((((triple7) -> (rule5 % int3)) ((triple7 ((triple7) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3