Anne is blue. Anne is green. Charlie is big. Charlie is blue. Charlie is nice. Charlie is not quiet. Gary is green. All round things are not quiet. All big things are not quiet. If Gary is not green then Gary is round. Green things are big. If something is nice and not smart then it is not big. All big things are nice. If Anne is smart and Anne is green then Anne is not nice. If Anne is not big then Anne is not blue.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is green.
("Anne" "is" "green" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
Gary is green.
("Gary" "is" "green" "+")
All round things are not quiet.
((("something" "is" "round" "+")) -> ("something" "is" "quiet" "-"))
All big things are not quiet.
((("something" "is" "big" "+")) -> ("something" "is" "quiet" "-"))
If Gary is not green then Gary is round.
((("Gary" "is" "green" "~")) -> ("Gary" "is" "round" "+"))
Green things are big.
((("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
If something is nice and not smart then it is not big.
((("something" "is" "nice" "+") ("something" "is" "smart" "~")) -> ("something" "is" "big" "-"))
All big things are nice.
((("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
If Anne is smart and Anne is green then Anne is not nice.
((("Anne" "is" "smart" "+") ("Anne" "is" "green" "+")) -> ("Anne" "is" "nice" "-"))
If Anne is not big then Anne is not blue.
((("Anne" "is" "big" "~")) -> ("Anne" "is" "blue" "-"))
Charlie is big.
True
1
proof
[(triple3)]
("Charlie" "is" "big" "+")
triple3
Charlie is quiet.
False
1
inv-proof
[(triple6 OR ((triple3) -> rule2))]
("Charlie" "is" "quiet" "+")
triple6
((triple3) -> (rule2 % int1))
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int1
Anne is big.
True
2
proof
[(((triple2) -> rule4))]
("Anne" "is" "big" "+")
((triple2) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Gary is not big.
False
2
inv-proof
[(((triple7) -> rule4))]
("Gary" "is" "big" "-")
((triple7) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is nice.
True
3
proof
[(((((triple7) -> rule4)) -> rule6))]
("Gary" "is" "nice" "+")
((((triple7) -> (rule4 % int2))) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is not nice.
False
3
inv-proof
[(((((triple7) -> rule4)) -> rule6))]
("Gary" "is" "nice" "-")
((((triple7) -> (rule4 % int2))) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is not round.
Unknown
inv-rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "round" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
Gary is not smart.
Unknown
inv-random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
Charlie is not green.
Unknown
inv-random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
@0: Anne is blue.[(triple1)] Anne is green.[(triple2)] Charlie is big.[(triple3)] Charlie is blue.[(triple4)] Charlie is nice.[(triple5 OR ((triple3) -> rule6))] Charlie is not quiet.[(triple6 OR ((triple3) -> rule2))] Gary is green.[(triple7)] @1: Anne is big.[(((triple2) -> rule4))] Gary is big.[(((triple7) -> rule4))] @2: Anne is nice.[(((((triple2) -> rule4)) -> rule6))] Anne is not quiet.[(((((triple2) -> rule4)) -> rule2))] Gary is nice.[(((((triple7) -> rule4)) -> rule6))] Gary is not quiet.[(((((triple7) -> rule4)) -> rule2))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
Charlie is big.
("Charlie" "is" "big" "+")
triple3
Charlie is blue.
("Charlie" "is" "blue" "+")
triple4
Charlie is nice.
("Charlie" "is" "nice" "+")
triple5
((triple3) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
triple6
((triple3) -> (rule2 % int1))
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int1
Gary is green.
("Gary" "is" "green" "+")
triple7
Anne is big.
("Anne" "is" "big" "+")
((triple2) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((triple7) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is not quiet.
("Anne" "is" "quiet" "-")
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Anne is not quiet.
("Anne" "is" "quiet" "-")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
((((triple7) -> (rule4 % int2))) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is not quiet.
("Gary" "is" "quiet" "-")
((((triple7) -> (rule4 % int2))) -> (rule2 % int1))
Gary is not quiet.
("Gary" "is" "quiet" "-")
int1
Gary is big.
("Gary" "is" "big" "+")
int2