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