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