Anne is blue. Anne is cold. Anne is furry. Anne is nice. Anne is rough. Charlie is cold. Charlie is furry. Charlie is rough. Harry is blue. Harry is smart. If Anne is blue then Anne is furry. All nice, blue things are cold. Green, nice things are smart. Nice, cold things are smart. If Anne is smart and Anne is rough then Anne is furry. If something is cold and rough then it is nice. If something is cold and smart then it is blue. If Anne is cold and Anne is nice then Anne is blue.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If Anne is blue then Anne is furry.
((("Anne" "is" "blue" "+")) -> ("Anne" "is" "furry" "+"))
All nice, blue things are cold.
((("something" "is" "nice" "+") ("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
Green, nice things are smart.
((("something" "is" "green" "+") ("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
Nice, cold things are smart.
((("something" "is" "nice" "+") ("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
If Anne is smart and Anne is rough then Anne is furry.
((("Anne" "is" "smart" "+") ("Anne" "is" "rough" "+")) -> ("Anne" "is" "furry" "+"))
If something is cold and rough then it is nice.
((("something" "is" "cold" "+") ("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
If something is cold and smart then it is blue.
((("something" "is" "cold" "+") ("something" "is" "smart" "+")) -> ("something" "is" "blue" "+"))
If Anne is cold and Anne is nice then Anne is blue.
((("Anne" "is" "cold" "+") ("Anne" "is" "nice" "+")) -> ("Anne" "is" "blue" "+"))
Charlie is rough.
True
1
proof
[(triple8)]
("Charlie" "is" "rough" "+")
triple8
Anne is not cold.
False
1
inv-proof
[(triple2 OR ((triple4 triple1) -> rule2))]
("Anne" "is" "cold" "-")
triple2
((triple4 triple1) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is smart.
True
3
proof
[(((triple4 triple2) -> rule4) OR ((triple4 ((triple4 triple1) -> rule2)) -> rule4) OR ((((triple2 triple5) -> rule6) triple2) -> rule4) OR ((((triple2 triple5) -> rule6) ((triple4 triple1) -> rule2)) -> rule4))]
("Anne" "is" "smart" "+")
((triple4 triple2) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((triple4 ((triple4 triple1) -> (rule2 % int2))) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
((((triple2 triple5) -> (rule6 % int2)) triple2) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
((((triple2 triple5) -> (rule6 % int3)) ((triple4 triple1) -> (rule2 % int2))) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is not smart.
False
3
inv-proof
[(((triple4 triple2) -> rule4) OR ((triple4 ((triple4 triple1) -> rule2)) -> rule4) OR ((((triple2 triple5) -> rule6) triple2) -> rule4) OR ((((triple2 triple5) -> rule6) ((triple4 triple1) -> rule2)) -> rule4))]
("Anne" "is" "smart" "-")
((triple4 triple2) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((triple4 ((triple4 triple1) -> (rule2 % int2))) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
((((triple2 triple5) -> (rule6 % int2)) triple2) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
((((triple2 triple5) -> (rule6 % int3)) ((triple4 triple1) -> (rule2 % int2))) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Charlie is smart.
True
5
proof
[(((((triple6 triple8) -> rule6) triple6) -> rule4))]
("Charlie" "is" "smart" "+")
((((triple6 triple8) -> (rule6 % int2)) triple6) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is not smart.
False
5
inv-proof
[(((((triple6 triple8) -> rule6) triple6) -> rule4))]
("Charlie" "is" "smart" "-")
((((triple6 triple8) -> (rule6 % int2)) triple6) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is blue.
True
7
proof
[(((triple6 ((((triple6 triple8) -> rule6) triple6) -> rule4)) -> rule7))]
("Charlie" "is" "blue" "+")
((triple6 ((((triple6 triple8) -> (rule6 % int3)) triple6) -> (rule4 % int2))) -> (rule7 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is not blue.
False
7
inv-proof
[(((triple6 ((((triple6 triple8) -> rule6) triple6) -> rule4)) -> rule7))]
("Charlie" "is" "blue" "-")
((triple6 ((((triple6 triple8) -> (rule6 % int3)) triple6) -> (rule4 % int2))) -> (rule7 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Harry is not cold.
Unknown
inv-rconc
[@2: Harry is cold.[CWA. Example of deepest failure = (rule2 <- rule6 <- FAIL)]]
("Harry" "is" "cold" "-")
Harry is nice.
Unknown
rconc
[@1: Harry is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "nice" "+")
Harry is not rough.
Unknown
inv-random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
@0: Anne is blue.[(triple1 OR ((triple2 triple4) -> rule8) OR ((triple2 ((triple2 triple5) -> rule6)) -> rule8) OR ((triple2 ((triple4 triple2) -> rule4)) -> rule7) OR ((triple2 ((((triple2 triple5) -> rule6) triple2) -> rule4)) -> rule7))] Anne is cold.[(triple2 OR ((triple4 triple1) -> rule2))] Anne is furry.[(triple3 OR ((triple1) -> rule1) OR ((((triple2 triple4) -> rule8)) -> rule1) OR ((((triple4 triple2) -> rule4) triple5) -> rule5) OR ((((triple2 ((triple2 triple5) -> rule6)) -> rule8)) -> rule1) OR ((((triple2 ((triple4 triple2) -> rule4)) -> rule7)) -> rule1) OR ((((triple4 ((triple4 triple1) -> rule2)) -> rule4) triple5) -> rule5) OR ((((((triple2 triple5) -> rule6) triple2) -> rule4) triple5) -> rule5) OR ((((((triple2 triple5) -> rule6) ((triple4 triple1) -> rule2)) -> rule4) triple5) -> rule5) OR ((((triple2 ((((triple2 triple5) -> rule6) triple2) -> rule4)) -> rule7)) -> rule1))] Anne is nice.[(triple4 OR ((triple2 triple5) -> rule6))] Anne is rough.[(triple5)] Charlie is cold.[(triple6)] Charlie is furry.[(triple7)] Charlie is rough.[(triple8)] Harry is blue.[(triple9)] Harry is smart.[(triple10)] @1: Anne is smart.[(((triple4 triple2) -> rule4) OR ((triple4 ((triple4 triple1) -> rule2)) -> rule4) OR ((((triple2 triple5) -> rule6) triple2) -> rule4) OR ((((triple2 triple5) -> rule6) ((triple4 triple1) -> rule2)) -> rule4))] Charlie is nice.[(((triple6 triple8) -> rule6))] @2: Charlie is smart.[(((((triple6 triple8) -> rule6) triple6) -> rule4))] @3: Charlie is blue.[(((triple6 ((((triple6 triple8) -> rule6) triple6) -> rule4)) -> rule7))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
((triple2 triple4) -> (rule8 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((triple2 ((triple2 triple5) -> (rule6 % int2))) -> (rule8 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
((triple2 ((triple4 triple2) -> (rule4 % int2))) -> (rule7 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
((triple2 ((((triple2 triple5) -> (rule6 % int3)) triple2) -> (rule4 % int2))) -> (rule7 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
triple2
((triple4 triple1) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
triple3
((triple1) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((((triple2 triple4) -> (rule8 % int2))) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
((((triple4 triple2) -> (rule4 % int2)) triple5) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
((((triple2 ((triple2 triple5) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
((((triple2 ((triple4 triple2) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
((((triple4 ((triple4 triple1) -> (rule2 % int3))) -> (rule4 % int2)) triple5) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
((((((triple2 triple5) -> (rule6 % int3)) triple2) -> (rule4 % int2)) triple5) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
((((((triple2 triple5) -> (rule6 % int4)) ((triple4 triple1) -> (rule2 % int3))) -> (rule4 % int2)) triple5) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
int4
((((triple2 ((((triple2 triple5) -> (rule6 % int4)) triple2) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
int4
Anne is nice.
("Anne" "is" "nice" "+")
triple4
((triple2 triple5) -> (rule6 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
triple5
Charlie is cold.
("Charlie" "is" "cold" "+")
triple6
Charlie is furry.
("Charlie" "is" "furry" "+")
triple7
Charlie is rough.
("Charlie" "is" "rough" "+")
triple8
Harry is blue.
("Harry" "is" "blue" "+")
triple9
Harry is smart.
("Harry" "is" "smart" "+")
triple10
Anne is smart.
("Anne" "is" "smart" "+")
((triple4 triple2) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((triple4 ((triple4 triple1) -> (rule2 % int2))) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
((((triple2 triple5) -> (rule6 % int2)) triple2) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
((((triple2 triple5) -> (rule6 % int3)) ((triple4 triple1) -> (rule2 % int2))) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple6 triple8) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((((triple6 triple8) -> (rule6 % int2)) triple6) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple6 ((((triple6 triple8) -> (rule6 % int3)) triple6) -> (rule4 % int2))) -> (rule7 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3