Charlie is round. Charlie is young. Erin is cold. Erin is furry. Erin is rough. Erin is white. Erin is young. Gary is round. Gary is white. Harry is cold. Harry is furry. Harry is rough. Young things are cold. White things are young. All round, young things are cold. All rough things are furry. Round things are white. If Gary is cold and Gary is white then Gary is round.
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Young things are cold.
((("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
White things are young.
((("something" "is" "white" "+")) -> ("something" "is" "young" "+"))
All round, young things are cold.
((("something" "is" "round" "+") ("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
All rough things are furry.
((("something" "is" "rough" "+")) -> ("something" "is" "furry" "+"))
Round things are white.
((("something" "is" "round" "+")) -> ("something" "is" "white" "+"))
If Gary is cold and Gary is white then Gary is round.
((("Gary" "is" "cold" "+") ("Gary" "is" "white" "+")) -> ("Gary" "is" "round" "+"))
Erin is furry.
True
1
proof
[(triple4 OR ((triple5) -> rule4))]
("Erin" "is" "furry" "+")
triple4
((triple5) -> (rule4 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is not cold.
False
1
inv-proof
[(triple3 OR ((triple7) -> rule1) OR ((((triple6) -> rule2)) -> rule1))]
("Erin" "is" "cold" "-")
triple3
((triple7) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Gary is young.
True
2
proof
[(((triple9) -> rule2) OR ((((triple8) -> rule5)) -> rule2))]
("Gary" "is" "young" "+")
((triple9) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
((((triple8) -> (rule5 % int2))) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is not young.
False
2
inv-proof
[(((triple9) -> rule2) OR ((((triple8) -> rule5)) -> rule2))]
("Gary" "is" "young" "-")
((triple9) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
((((triple8) -> (rule5 % int2))) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is cold.
True
3
proof
[(((((triple9) -> rule2)) -> rule1) OR ((triple8 ((triple9) -> rule2)) -> rule3) OR ((((((triple8) -> rule5)) -> rule2)) -> rule1) OR ((triple8 ((((triple8) -> rule5)) -> rule2)) -> rule3))]
("Gary" "is" "cold" "+")
((((triple9) -> (rule2 % int2))) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
((triple8 ((triple9) -> (rule2 % int2))) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
((((((triple8) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
((triple8 ((((triple8) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is not cold.
False
3
inv-proof
[(((((triple9) -> rule2)) -> rule1) OR ((triple8 ((triple9) -> rule2)) -> rule3) OR ((((((triple8) -> rule5)) -> rule2)) -> rule1) OR ((triple8 ((((triple8) -> rule5)) -> rule2)) -> rule3))]
("Gary" "is" "cold" "-")
((((triple9) -> (rule2 % int2))) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
((triple8 ((triple9) -> (rule2 % int2))) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
((((((triple8) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
((triple8 ((((triple8) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Harry is not young.
Unknown
inv-rconc
[@2: Harry is young.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("Harry" "is" "young" "-")
Harry is white.
Unknown
rconc
[@1: Harry is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "white" "+")
Gary is not furry.
Unknown
inv-rconc
[@1: Gary is furry.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "furry" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
Erin is not round.
Unknown
inv-random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
@0: Charlie is round.[(triple1)] Charlie is young.[(triple2 OR ((((triple1) -> rule5)) -> rule2))] Erin is cold.[(triple3 OR ((triple7) -> rule1) OR ((((triple6) -> rule2)) -> rule1))] Erin is furry.[(triple4 OR ((triple5) -> rule4))] Erin is rough.[(triple5)] Erin is white.[(triple6)] Erin is young.[(triple7 OR ((triple6) -> rule2))] Gary is round.[(triple8 OR ((((((triple9) -> rule2)) -> rule1) triple9) -> rule6))] Gary is white.[(triple9 OR ((triple8) -> rule5))] Harry is cold.[(triple10)] Harry is furry.[(triple11 OR ((triple12) -> rule4))] Harry is rough.[(triple12)] @1: Charlie is cold.[(((triple2) -> rule1) OR ((triple1 triple2) -> rule3) OR ((((((triple1) -> rule5)) -> rule2)) -> rule1) OR ((triple1 ((((triple1) -> rule5)) -> rule2)) -> rule3))] Charlie is white.[(((triple1) -> rule5))] Gary is young.[(((triple9) -> rule2) OR ((((triple8) -> rule5)) -> rule2))] @2: Gary is cold.[(((((triple9) -> rule2)) -> rule1) OR ((triple8 ((triple9) -> rule2)) -> rule3) OR ((((((triple8) -> rule5)) -> rule2)) -> rule1) OR ((triple8 ((((triple8) -> rule5)) -> rule2)) -> rule3))]
Charlie is round.
("Charlie" "is" "round" "+")
triple1
Charlie is young.
("Charlie" "is" "young" "+")
triple2
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
triple3
((triple7) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
triple4
((triple5) -> (rule4 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
triple5
Erin is white.
("Erin" "is" "white" "+")
triple6
Erin is young.
("Erin" "is" "young" "+")
triple7
((triple6) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
triple8
((((((triple9) -> (rule2 % int3))) -> (rule1 % int2)) triple9) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
triple9
((triple8) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
triple10
Harry is furry.
("Harry" "is" "furry" "+")
triple11
((triple12) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
triple12
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple2) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((triple1 triple2) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
((triple1 ((((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
((triple1) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((triple9) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
((((triple8) -> (rule5 % int2))) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
((((triple9) -> (rule2 % int2))) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
((triple8 ((triple9) -> (rule2 % int2))) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
((((((triple8) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
((triple8 ((((triple8) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3