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