Anne is kind. Anne is quiet. Anne is round. Anne is smart. Anne is white. Bob is cold. Bob is kind. Gary is cold. Gary is green. Gary is round. Harry is cold. Harry is green. Harry is kind. Harry is quiet. Harry is round. Harry is smart. Cold, smart people are green. All cold people are smart. Kind, quiet people are white. Green people are quiet. All quiet people are smart. If someone is white then they are cold.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is white.
("Anne" "is" "white" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Cold, smart people are green.
((("someone" "is" "cold" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
All cold people are smart.
((("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "+"))
Kind, quiet people are white.
((("someone" "is" "kind" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
Green people are quiet.
((("someone" "is" "green" "+")) -> ("someone" "is" "quiet" "+"))
All quiet people are smart.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
If someone is white then they are cold.
((("someone" "is" "white" "+")) -> ("someone" "is" "cold" "+"))
Harry is cold.
True
1
proof
[(triple11 OR ((((triple13 triple14) -> rule3)) -> rule6) OR ((((triple13 ((triple12) -> rule4)) -> rule3)) -> rule6))]
("Harry" "is" "cold" "+")
triple11
((((triple13 triple14) -> (rule3 % int2))) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((((triple13 ((triple12) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is not cold.
False
1
inv-proof
[(triple11 OR ((((triple13 triple14) -> rule3)) -> rule6) OR ((((triple13 ((triple12) -> rule4)) -> rule3)) -> rule6))]
("Harry" "is" "cold" "-")
triple11
((((triple13 triple14) -> (rule3 % int2))) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((((triple13 ((triple12) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Gary is not white.
Unknown
inv-rconc
[@1: Gary is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "white" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
@0: Anne is kind.[(triple1)] Anne is quiet.[(triple2 OR ((((((triple5) -> rule6) triple4) -> rule1)) -> rule4) OR ((((((triple5) -> rule6) ((((triple5) -> rule6)) -> rule2)) -> rule1)) -> rule4))] Anne is round.[(triple3)] Anne is smart.[(triple4 OR ((triple2) -> rule5) OR ((((triple5) -> rule6)) -> rule2) OR ((((((triple1 triple2) -> rule3)) -> rule6)) -> rule2))] Anne is white.[(triple5 OR ((triple1 triple2) -> rule3))] Bob is cold.[(triple6)] Bob is kind.[(triple7)] Gary is cold.[(triple8)] Gary is green.[(triple9 OR ((triple8 ((triple8) -> rule2)) -> rule1))] Gary is round.[(triple10)] Harry is cold.[(triple11 OR ((((triple13 triple14) -> rule3)) -> rule6) OR ((((triple13 ((triple12) -> rule4)) -> rule3)) -> rule6))] Harry is green.[(triple12 OR ((triple11 triple16) -> rule1) OR ((triple11 ((triple11) -> rule2)) -> rule1) OR ((triple11 ((triple14) -> rule5)) -> rule1) OR ((((((triple13 triple14) -> rule3)) -> rule6) triple16) -> rule1) OR ((((((triple13 triple14) -> rule3)) -> rule6) ((triple11) -> rule2)) -> rule1) OR ((((((triple13 triple14) -> rule3)) -> rule6) ((triple14) -> rule5)) -> rule1) OR ((triple11 ((((((triple13 triple14) -> rule3)) -> rule6)) -> rule2)) -> rule1) OR ((((((triple13 triple14) -> rule3)) -> rule6) ((((((triple13 triple14) -> rule3)) -> rule6)) -> rule2)) -> rule1))] Harry is kind.[(triple13)] Harry is quiet.[(triple14 OR ((triple12) -> rule4) OR ((((triple11 triple16) -> rule1)) -> rule4) OR ((((triple11 ((triple11) -> rule2)) -> rule1)) -> rule4))] Harry is round.[(triple15)] Harry is smart.[(triple16 OR ((triple11) -> rule2) OR ((triple14) -> rule5) OR ((((triple12) -> rule4)) -> rule5) OR ((((((triple13 triple14) -> rule3)) -> rule6)) -> rule2) OR ((((((triple13 ((triple12) -> rule4)) -> rule3)) -> rule6)) -> rule2))] @1: Anne is cold.[(((triple5) -> rule6) OR ((((triple1 triple2) -> rule3)) -> rule6))] Bob is smart.[(((triple6) -> rule2))] Gary is quiet.[(((triple9) -> rule4) OR ((((triple8 ((triple8) -> rule2)) -> rule1)) -> rule4))] Gary is smart.[(((triple8) -> rule2) OR ((((triple9) -> rule4)) -> rule5))] Harry is white.[(((triple13 triple14) -> rule3) OR ((triple13 ((triple12) -> rule4)) -> rule3) OR ((triple13 ((((triple11 triple16) -> rule1)) -> rule4)) -> rule3) OR ((triple13 ((((triple11 ((triple11) -> rule2)) -> rule1)) -> rule4)) -> rule3))] @2: Anne is green.[(((((triple5) -> rule6) triple4) -> rule1) OR ((((triple5) -> rule6) ((triple2) -> rule5)) -> rule1) OR ((((((triple1 triple2) -> rule3)) -> rule6) triple4) -> rule1) OR ((((triple5) -> rule6) ((((triple5) -> rule6)) -> rule2)) -> rule1) OR ((((((triple1 triple2) -> rule3)) -> rule6) ((triple2) -> rule5)) -> rule1) OR ((((((triple1 triple2) -> rule3)) -> rule6) ((((triple5) -> rule6)) -> rule2)) -> rule1) OR ((((triple5) -> rule6) ((((((triple1 triple2) -> rule3)) -> rule6)) -> rule2)) -> rule1) OR ((((((triple1 triple2) -> rule3)) -> rule6) ((((((triple1 triple2) -> rule3)) -> rule6)) -> rule2)) -> rule1))] Bob is green.[(((triple6 ((triple6) -> rule2)) -> rule1))] @3: Bob is quiet.[(((((triple6 ((triple6) -> rule2)) -> rule1)) -> rule4))] @4: Bob is white.[(((triple7 ((((triple6 ((triple6) -> rule2)) -> rule1)) -> rule4)) -> rule3))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
((((((triple5) -> (rule6 % int3)) triple4) -> (rule1 % int2))) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
((((((triple5) -> (rule6 % int4)) ((((triple5) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
int4
Anne is round.
("Anne" "is" "round" "+")
triple3
Anne is smart.
("Anne" "is" "smart" "+")
triple4
((triple2) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((((triple5) -> (rule6 % int2))) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
((((((triple1 triple2) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
triple5
((triple1 triple2) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
triple6
Bob is kind.
("Bob" "is" "kind" "+")
triple7
Gary is cold.
("Gary" "is" "cold" "+")
triple8
Gary is green.
("Gary" "is" "green" "+")
triple9
((triple8 ((triple8) -> (rule2 % int2))) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
triple10
Harry is cold.
("Harry" "is" "cold" "+")
triple11
((((triple13 triple14) -> (rule3 % int2))) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((((triple13 ((triple12) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
triple12
((triple11 triple16) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((triple11 ((triple11) -> (rule2 % int2))) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((triple11 ((triple14) -> (rule5 % int2))) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((((((triple13 triple14) -> (rule3 % int3))) -> (rule6 % int2)) triple16) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
((((((triple13 triple14) -> (rule3 % int4))) -> (rule6 % int3)) ((triple11) -> (rule2 % int2))) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
int4
((((((triple13 triple14) -> (rule3 % int4))) -> (rule6 % int3)) ((triple14) -> (rule5 % int2))) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
int4
((triple11 ((((((triple13 triple14) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
int4
((((((triple13 triple14) -> (rule3 % int4))) -> (rule6 % int3)) ((((((triple13 triple14) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
int4
Harry is kind.
("Harry" "is" "kind" "+")
triple13
Harry is quiet.
("Harry" "is" "quiet" "+")
triple14
((triple12) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((((triple11 triple16) -> (rule1 % int2))) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((triple11 ((triple11) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
triple15
Harry is smart.
("Harry" "is" "smart" "+")
triple16
((triple11) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((triple14) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((((triple12) -> (rule4 % int2))) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((((triple13 triple14) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
((((((triple13 ((triple12) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
int4
Anne is cold.
("Anne" "is" "cold" "+")
((triple5) -> (rule6 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((((triple1 triple2) -> (rule3 % int2))) -> (rule6 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
((triple6) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple9) -> (rule4 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((((triple8 ((triple8) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
((triple8) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((((triple9) -> (rule4 % int2))) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
((triple13 triple14) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((triple13 ((triple12) -> (rule4 % int2))) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((triple13 ((((triple11 triple16) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
((triple13 ((((triple11 ((triple11) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4
Anne is green.
("Anne" "is" "green" "+")
((((triple5) -> (rule6 % int2)) triple4) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
((((triple5) -> (rule6 % int3)) ((triple2) -> (rule5 % int2))) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
((((((triple1 triple2) -> (rule3 % int3))) -> (rule6 % int2)) triple4) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
((((triple5) -> (rule6 % int3)) ((((triple5) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
((((((triple1 triple2) -> (rule3 % int4))) -> (rule6 % int3)) ((triple2) -> (rule5 % int2))) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
int4
((((((triple1 triple2) -> (rule3 % int4))) -> (rule6 % int3)) ((((triple5) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
int4
((((triple5) -> (rule6 % int4)) ((((((triple1 triple2) -> (rule3 % int3))) -> (rule6 % int4))) -> (rule2 % int2))) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
int4
((((((triple1 triple2) -> (rule3 % int4))) -> (rule6 % int3)) ((((((triple1 triple2) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
int4
Bob is green.
("Bob" "is" "green" "+")
((triple6 ((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
((((triple6 ((triple6) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
((triple7 ((((triple6 ((triple6) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4