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