Anne is cold. Charlie is green. Gary is round. Harry is green. If something is big and not green then it is not cold. If Anne is green and Anne is big then Anne is blue. If Charlie is red then Charlie is not round. If something is green and big then it is red. Green things are big. If Charlie is green and Charlie is blue then Charlie is not red.
Anne is cold.
("Anne" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is green.
("Harry" "is" "green" "+")
If something is big and not green then it is not cold.
((("something" "is" "big" "+") ("something" "is" "green" "~")) -> ("something" "is" "cold" "-"))
If Anne is green and Anne is big then Anne is blue.
((("Anne" "is" "green" "+") ("Anne" "is" "big" "+")) -> ("Anne" "is" "blue" "+"))
If Charlie is red then Charlie is not round.
((("Charlie" "is" "red" "+")) -> ("Charlie" "is" "round" "-"))
If something is green and big then it is red.
((("something" "is" "green" "+") ("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
Green things are big.
((("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
If Charlie is green and Charlie is blue then Charlie is not red.
((("Charlie" "is" "green" "+") ("Charlie" "is" "blue" "+")) -> ("Charlie" "is" "red" "-"))
Charlie is green.
True
1
proof
[(triple2)]
("Charlie" "is" "green" "+")
triple2
Gary is not round.
False
1
inv-proof
[(triple3)]
("Gary" "is" "round" "-")
triple3
Harry is big.
True
2
proof
[(((triple4) -> rule5))]
("Harry" "is" "big" "+")
((triple4) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Charlie is not big.
False
2
inv-proof
[(((triple2) -> rule5))]
("Charlie" "is" "big" "-")
((triple2) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Harry is red.
True
4
proof
[(((triple4 ((triple4) -> rule5)) -> rule4))]
("Harry" "is" "red" "+")
((triple4 ((triple4) -> (rule5 % int2))) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is not red.
False
4
inv-proof
[(((triple4 ((triple4) -> rule5)) -> rule4))]
("Harry" "is" "red" "-")
((triple4 ((triple4) -> (rule5 % int2))) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Charlie is not round.
True
5
proof
[(((((triple2 ((triple2) -> rule5)) -> rule4)) -> rule3))]
("Charlie" "is" "round" "-")
((((triple2 ((triple2) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is not round.
("Charlie" "is" "round" "-")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is round.
False
5
inv-proof
[(((((triple2 ((triple2) -> rule5)) -> rule4)) -> rule3))]
("Charlie" "is" "round" "+")
((((triple2 ((triple2) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is not round.
("Charlie" "is" "round" "-")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Gary is not big.
Unknown
inv-rconc
[@1: Gary is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "big" "-")
Anne is big.
Unknown
rconc
[@1: Anne is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "big" "+")
Anne is not blue.
Unknown
inv-rconc
[@1: Anne is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "blue" "-")
Anne is red.
Unknown
rconc
[@1: Anne is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "red" "+")
Gary is not furry.
Unknown
inv-random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
Gary is not blue.
Unknown
inv-random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
@0: Anne is cold.[(triple1)] Charlie is green.[(triple2)] Gary is round.[(triple3)] Harry is green.[(triple4)] @1: Charlie is big.[(((triple2) -> rule5))] Harry is big.[(((triple4) -> rule5))] @2: Charlie is red.[(((triple2 ((triple2) -> rule5)) -> rule4))] Harry is red.[(((triple4 ((triple4) -> rule5)) -> rule4))] @3: Charlie is not round.[(((((triple2 ((triple2) -> rule5)) -> rule4)) -> rule3))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Gary is round.
("Gary" "is" "round" "+")
triple3
Harry is green.
("Harry" "is" "green" "+")
triple4
Charlie is big.
("Charlie" "is" "big" "+")
((triple2) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple4) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((triple2 ((triple2) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
((triple4 ((triple4) -> (rule5 % int2))) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Charlie is not round.
("Charlie" "is" "round" "-")
((((triple2 ((triple2) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is not round.
("Charlie" "is" "round" "-")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3