Anne is smart. Bob is green. Bob is kind. Bob is red. Charlie is green. Charlie is quiet. Gary is green. Gary is quiet. Gary is red. Gary is round. Kind people are red. If Charlie is red and Charlie is kind then Charlie is smart. Red, smart people are kind. All round people are quiet. All quiet people are green. Quiet, green people are red. If someone is quiet then they are round. If Anne is white and Anne is green then Anne is kind.
Anne is smart.
("Anne" "is" "smart" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is red.
("Bob" "is" "red" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is round.
("Gary" "is" "round" "+")
Kind people are red.
((("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
If Charlie is red and Charlie is kind then Charlie is smart.
((("Charlie" "is" "red" "+") ("Charlie" "is" "kind" "+")) -> ("Charlie" "is" "smart" "+"))
Red, smart people are kind.
((("someone" "is" "red" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "kind" "+"))
All round people are quiet.
((("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
All quiet people are green.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
Quiet, green people are red.
((("someone" "is" "quiet" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
If someone is quiet then they are round.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
If Anne is white and Anne is green then Anne is kind.
((("Anne" "is" "white" "+") ("Anne" "is" "green" "+")) -> ("Anne" "is" "kind" "+"))
Bob is green.
True
1
proof
[(triple2)]
("Bob" "is" "green" "+")
triple2
Gary is not quiet.
False
1
inv-proof
[(triple8 OR ((triple10) -> rule4))]
("Gary" "is" "quiet" "-")
triple8
((triple10) -> (rule4 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Anne is not kind.
Unknown
inv-rconc
[@4: Anne is kind.[CWA. Example of deepest failure = (rule3 <- rule6 <- rule4 <- rule7 <- FAIL)]]
("Anne" "is" "kind" "-")
Charlie is white.
Unknown
random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "+")
@0: Anne is smart.[(triple1)] Bob is green.[(triple2)] Bob is kind.[(triple3)] Bob is red.[(triple4 OR ((triple3) -> rule1))] Charlie is green.[(triple5 OR ((triple6) -> rule5))] Charlie is quiet.[(triple6)] Gary is green.[(triple7 OR ((triple8) -> rule5) OR ((((triple10) -> rule4)) -> rule5))] Gary is quiet.[(triple8 OR ((triple10) -> rule4))] Gary is red.[(triple9 OR ((triple8 triple7) -> rule6) OR ((triple8 ((triple8) -> rule5)) -> rule6) OR ((((triple10) -> rule4) triple7) -> rule6) OR ((((triple10) -> rule4) ((triple8) -> rule5)) -> rule6) OR ((triple8 ((((triple10) -> rule4)) -> rule5)) -> rule6) OR ((((triple10) -> rule4) ((((triple10) -> rule4)) -> rule5)) -> rule6))] Gary is round.[(triple10 OR ((triple8) -> rule7))] @1: Charlie is red.[(((triple6 triple5) -> rule6) OR ((triple6 ((triple6) -> rule5)) -> rule6))] Charlie is round.[(((triple6) -> rule7))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Bob is red.
("Bob" "is" "red" "+")
triple4
((triple3) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
triple5
((triple6) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple6
Gary is green.
("Gary" "is" "green" "+")
triple7
((triple8) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((((triple10) -> (rule4 % int2))) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
triple8
((triple10) -> (rule4 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
triple9
((triple8 triple7) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((triple8 ((triple8) -> (rule5 % int2))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
((((triple10) -> (rule4 % int2)) triple7) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
((((triple10) -> (rule4 % int3)) ((triple8) -> (rule5 % int2))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
((triple8 ((((triple10) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
((((triple10) -> (rule4 % int3)) ((((triple10) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
triple10
((triple8) -> (rule7 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((triple6 triple5) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((triple6 ((triple6) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
((triple6) -> (rule7 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1