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