Anne is cold. Anne is green. Anne is kind. Anne is quiet. Dave is smart. Gary is cold. Gary is green. Gary is smart. Harry is big. Harry is red. Red, green things are kind. All quiet, big things are cold. If Dave is kind and Dave is quiet then Dave is cold. All big things are green. Quiet, green things are red. All green things are quiet.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is red.
("Harry" "is" "red" "+")
Red, green things are kind.
((("something" "is" "red" "+") ("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
All quiet, big things are cold.
((("something" "is" "quiet" "+") ("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
If Dave is kind and Dave is quiet then Dave is cold.
((("Dave" "is" "kind" "+") ("Dave" "is" "quiet" "+")) -> ("Dave" "is" "cold" "+"))
All big things are green.
((("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
Quiet, green things are red.
((("something" "is" "quiet" "+") ("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
All green things are quiet.
((("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
Gary is cold.
True
1
proof
[(triple6)]
("Gary" "is" "cold" "+")
triple6
Gary is not cold.
False
1
inv-proof
[(triple6)]
("Gary" "is" "cold" "-")
triple6
Anne is red.
True
3
proof
[(((triple4 triple2) -> rule5) OR ((((triple2) -> rule6) triple2) -> rule5))]
("Anne" "is" "red" "+")
((triple4 triple2) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((((triple2) -> (rule6 % int2)) triple2) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is not red.
False
3
inv-proof
[(((triple4 triple2) -> rule5) OR ((((triple2) -> rule6) triple2) -> rule5))]
("Anne" "is" "red" "-")
((triple4 triple2) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((((triple2) -> (rule6 % int2)) triple2) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Gary is red.
True
4
proof
[(((((triple7) -> rule6) triple7) -> rule5))]
("Gary" "is" "red" "+")
((((triple7) -> (rule6 % int2)) triple7) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Harry is not quiet.
False
3
inv-proof
[(((((triple9) -> rule4)) -> rule6))]
("Harry" "is" "quiet" "-")
((((triple9) -> (rule4 % int2))) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Dave is not red.
Unknown
inv-rconc
[@2: Dave is red.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("Dave" "is" "red" "-")
Dave is green.
Unknown
rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "green" "+")
Dave is not quiet.
Unknown
inv-rconc
[@2: Dave is quiet.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("Dave" "is" "quiet" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
Gary is not big.
Unknown
inv-random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
@0: Anne is cold.[(triple1)] Anne is green.[(triple2)] Anne is kind.[(triple3 OR ((((triple4 triple2) -> rule5) triple2) -> rule1) OR ((((((triple2) -> rule6) triple2) -> rule5) triple2) -> rule1))] Anne is quiet.[(triple4 OR ((triple2) -> rule6))] Dave is smart.[(triple5)] Gary is cold.[(triple6)] Gary is green.[(triple7)] Gary is smart.[(triple8)] Harry is big.[(triple9)] Harry is red.[(triple10 OR ((((((triple9) -> rule4)) -> rule6) ((triple9) -> rule4)) -> rule5))] @1: Anne is red.[(((triple4 triple2) -> rule5) OR ((((triple2) -> rule6) triple2) -> rule5))] Gary is quiet.[(((triple7) -> rule6))] Harry is green.[(((triple9) -> rule4))] @2: Gary is red.[(((((triple7) -> rule6) triple7) -> rule5))] Harry is kind.[(((triple10 ((triple9) -> rule4)) -> rule1) OR ((((((((triple9) -> rule4)) -> rule6) ((triple9) -> rule4)) -> rule5) ((triple9) -> rule4)) -> rule1))] Harry is quiet.[(((((triple9) -> rule4)) -> rule6))] @3: Gary is kind.[(((((((triple7) -> rule6) triple7) -> rule5) triple7) -> rule1))] Harry is cold.[(((((((triple9) -> rule4)) -> rule6) triple9) -> rule2))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is kind.
("Anne" "is" "kind" "+")
triple3
((((triple4 triple2) -> (rule5 % int2)) triple2) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
((((((triple2) -> (rule6 % int3)) triple2) -> (rule5 % int2)) triple2) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
triple4
((triple2) -> (rule6 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
triple5
Gary is cold.
("Gary" "is" "cold" "+")
triple6
Gary is green.
("Gary" "is" "green" "+")
triple7
Gary is smart.
("Gary" "is" "smart" "+")
triple8
Harry is big.
("Harry" "is" "big" "+")
triple9
Harry is red.
("Harry" "is" "red" "+")
triple10
((((((triple9) -> (rule4 % int3))) -> (rule6 % int2)) ((triple9) -> (rule4 % int3))) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
((triple4 triple2) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((((triple2) -> (rule6 % int2)) triple2) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple7) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((triple9) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((((triple7) -> (rule6 % int2)) triple7) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
((triple10 ((triple9) -> (rule4 % int2))) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((((((triple9) -> (rule4 % int4))) -> (rule6 % int3)) ((triple9) -> (rule4 % int4))) -> (rule5 % int2)) ((triple9) -> (rule4 % int4))) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
int4
Harry is quiet.
("Harry" "is" "quiet" "+")
((((triple9) -> (rule4 % int2))) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
((((((triple7) -> (rule6 % int3)) triple7) -> (rule5 % int2)) triple7) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
((((((triple9) -> (rule4 % int3))) -> (rule6 % int2)) triple9) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3