Anne is cold. Anne is green. Anne is rough. Charlie is round. Dave is big. Dave is kind. Dave is round. Dave is smart. Erin is green. Erin is round. If something is cold then it is big. If Anne is cold and Anne is round then Anne is green. Green, round things are kind. If something is rough and round then it is smart. Kind things are green. Kind things are rough. If something is kind and big then it is cold. If Erin is kind and Erin is rough then Erin is round. If something is rough and smart then it is cold.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is round.
("Erin" "is" "round" "+")
If something is cold then it is big.
((("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
If Anne is cold and Anne is round then Anne is green.
((("Anne" "is" "cold" "+") ("Anne" "is" "round" "+")) -> ("Anne" "is" "green" "+"))
Green, round things are kind.
((("something" "is" "green" "+") ("something" "is" "round" "+")) -> ("something" "is" "kind" "+"))
If something is rough and round then it is smart.
((("something" "is" "rough" "+") ("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
Kind things are green.
((("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
Kind things are rough.
((("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
If something is kind and big then it is cold.
((("something" "is" "kind" "+") ("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
If Erin is kind and Erin is rough then Erin is round.
((("Erin" "is" "kind" "+") ("Erin" "is" "rough" "+")) -> ("Erin" "is" "round" "+"))
If something is rough and smart then it is cold.
((("something" "is" "rough" "+") ("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
Dave is kind.
True
1
proof
[(triple6)]
("Dave" "is" "kind" "+")
triple6
Charlie is not round.
False
1
inv-proof
[(triple4)]
("Charlie" "is" "round" "-")
triple4
Dave is rough.
True
2
proof
[(((triple6) -> rule6))]
("Dave" "is" "rough" "+")
((triple6) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is not green.
False
2
inv-proof
[(((triple6) -> rule5))]
("Dave" "is" "green" "-")
((triple6) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Erin is rough.
True
4
proof
[(((((triple9 triple10) -> rule3)) -> rule6))]
("Erin" "is" "rough" "+")
((((triple9 triple10) -> (rule3 % int2))) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is not rough.
False
4
inv-proof
[(((((triple9 triple10) -> rule3)) -> rule6))]
("Erin" "is" "rough" "-")
((((triple9 triple10) -> (rule3 % int2))) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is smart.
True
6
proof
[(((((((triple9 triple10) -> rule3)) -> rule6) triple10) -> rule4))]
("Erin" "is" "smart" "+")
((((((triple9 triple10) -> (rule3 % int3))) -> (rule6 % int2)) triple10) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is not smart.
False
6
inv-proof
[(((((((triple9 triple10) -> rule3)) -> rule6) triple10) -> rule4))]
("Erin" "is" "smart" "-")
((((((triple9 triple10) -> (rule3 % int3))) -> (rule6 % int2)) triple10) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is cold.
True
11
proof
[(((((((triple9 triple10) -> rule3)) -> rule6) ((((((triple9 triple10) -> rule3)) -> rule6) triple10) -> rule4)) -> rule9))]
("Erin" "is" "cold" "+")
((((((triple9 triple10) -> (rule3 % int4))) -> (rule6 % int3)) ((((((triple9 triple10) -> (rule3 % int4))) -> (rule6 % int3)) triple10) -> (rule4 % int2))) -> (rule9 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4
Erin is not cold.
False
11
inv-proof
[(((((((triple9 triple10) -> rule3)) -> rule6) ((((((triple9 triple10) -> rule3)) -> rule6) triple10) -> rule4)) -> rule9))]
("Erin" "is" "cold" "-")
((((((triple9 triple10) -> (rule3 % int4))) -> (rule6 % int3)) ((((((triple9 triple10) -> (rule3 % int4))) -> (rule6 % int3)) triple10) -> (rule4 % int2))) -> (rule9 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4
Erin is big.
True
12
proof
[(((((((((triple9 triple10) -> rule3)) -> rule6) ((((((triple9 triple10) -> rule3)) -> rule6) triple10) -> rule4)) -> rule9)) -> rule1))]
("Erin" "is" "big" "+")
((((((((triple9 triple10) -> (rule3 % int5))) -> (rule6 % int4)) ((((((triple9 triple10) -> (rule3 % int5))) -> (rule6 % int4)) triple10) -> (rule4 % int3))) -> (rule9 % int2))) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
int4
Erin is kind.
("Erin" "is" "kind" "+")
int5
Erin is not big.
False
12
inv-proof
[(((((((((triple9 triple10) -> rule3)) -> rule6) ((((((triple9 triple10) -> rule3)) -> rule6) triple10) -> rule4)) -> rule9)) -> rule1))]
("Erin" "is" "big" "-")
((((((((triple9 triple10) -> (rule3 % int5))) -> (rule6 % int4)) ((((((triple9 triple10) -> (rule3 % int5))) -> (rule6 % int4)) triple10) -> (rule4 % int3))) -> (rule9 % int2))) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
int4
Erin is kind.
("Erin" "is" "kind" "+")
int5
Anne is not kind.
Unknown
inv-rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "kind" "-")
Charlie is smart.
Unknown
rconc
[@4: Charlie is smart.[CWA. Example of deepest failure = (rule4 <- rule6 <- rule3 <- rule5 <- FAIL)]]
("Charlie" "is" "smart" "+")
Charlie is not green.
Unknown
inv-rconc
[@2: Charlie is green.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("Charlie" "is" "green" "-")
Charlie is kind.
Unknown
rconc
[@2: Charlie is kind.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("Charlie" "is" "kind" "+")
Charlie is not cold.
Unknown
inv-rconc
[@4: Charlie is cold.[CWA. Example of deepest failure = (rule9 <- rule6 <- rule3 <- rule5 <- FAIL)]]
("Charlie" "is" "cold" "-")
Anne is smart.
Unknown
rconc
[@1: Anne is smart.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "smart" "+")
@0: Anne is cold.[(triple1)] Anne is green.[(triple2)] Anne is rough.[(triple3)] Charlie is round.[(triple4)] Dave is big.[(triple5 OR ((((((triple6) -> rule6) triple8) -> rule9)) -> rule1) OR ((((((triple6) -> rule6) ((((triple6) -> rule6) triple7) -> rule4)) -> rule9)) -> rule1))] Dave is kind.[(triple6)] Dave is round.[(triple7)] Dave is smart.[(triple8 OR ((((triple6) -> rule6) triple7) -> rule4))] Erin is green.[(triple9)] Erin is round.[(triple10)] @1: Anne is big.[(((triple1) -> rule1))] Dave is cold.[(((triple6 triple5) -> rule7) OR ((((triple6) -> rule6) triple8) -> rule9) OR ((((triple6) -> rule6) ((((triple6) -> rule6) triple7) -> rule4)) -> rule9))] Dave is green.[(((triple6) -> rule5))] Dave is rough.[(((triple6) -> rule6))] Erin is kind.[(((triple9 triple10) -> rule3))] @2: Erin is rough.[(((((triple9 triple10) -> rule3)) -> rule6))] @3: Erin is smart.[(((((((triple9 triple10) -> rule3)) -> rule6) triple10) -> rule4))] @4: Erin is cold.[(((((((triple9 triple10) -> rule3)) -> rule6) ((((((triple9 triple10) -> rule3)) -> rule6) triple10) -> rule4)) -> rule9))] @5: Erin is big.[(((((((((triple9 triple10) -> rule3)) -> rule6) ((((((triple9 triple10) -> rule3)) -> rule6) triple10) -> rule4)) -> rule9)) -> rule1))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is rough.
("Anne" "is" "rough" "+")
triple3
Charlie is round.
("Charlie" "is" "round" "+")
triple4
Dave is big.
("Dave" "is" "big" "+")
triple5
((((((triple6) -> (rule6 % int3)) triple8) -> (rule9 % int2))) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
((((((triple6) -> (rule6 % int4)) ((((triple6) -> (rule6 % int4)) triple7) -> (rule4 % int3))) -> (rule9 % int2))) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Dave is kind.
("Dave" "is" "kind" "+")
triple6
Dave is round.
("Dave" "is" "round" "+")
triple7
Dave is smart.
("Dave" "is" "smart" "+")
triple8
((((triple6) -> (rule6 % int2)) triple7) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
triple9
Erin is round.
("Erin" "is" "round" "+")
triple10
Anne is big.
("Anne" "is" "big" "+")
((triple1) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
((triple6 triple5) -> (rule7 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((((triple6) -> (rule6 % int2)) triple8) -> (rule9 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
((((triple6) -> (rule6 % int3)) ((((triple6) -> (rule6 % int3)) triple7) -> (rule4 % int2))) -> (rule9 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
((triple6) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((triple6) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
((triple9 triple10) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
((((triple9 triple10) -> (rule3 % int2))) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
((((((triple9 triple10) -> (rule3 % int3))) -> (rule6 % int2)) triple10) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
((((((triple9 triple10) -> (rule3 % int4))) -> (rule6 % int3)) ((((((triple9 triple10) -> (rule3 % int4))) -> (rule6 % int3)) triple10) -> (rule4 % int2))) -> (rule9 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4
Erin is big.
("Erin" "is" "big" "+")
((((((((triple9 triple10) -> (rule3 % int5))) -> (rule6 % int4)) ((((((triple9 triple10) -> (rule3 % int5))) -> (rule6 % int4)) triple10) -> (rule4 % int3))) -> (rule9 % int2))) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
int4
Erin is kind.
("Erin" "is" "kind" "+")
int5