Anne is blue. Anne is rough. Bob is quiet. Bob is smart. Charlie is quiet. Charlie is white. Gary is quiet. Gary is rough. Gary is smart. Gary is white. Quiet things are round. If Charlie is rough and Charlie is white then Charlie is smart. All quiet, blue things are rough. If something is round then it is blue. If something is kind and rough then it is blue. All smart things are rough. If something is rough and blue then it is quiet. If something is quiet then it is blue.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
Quiet things are round.
((("something" "is" "quiet" "+")) -> ("something" "is" "round" "+"))
If Charlie is rough and Charlie is white then Charlie is smart.
((("Charlie" "is" "rough" "+") ("Charlie" "is" "white" "+")) -> ("Charlie" "is" "smart" "+"))
All quiet, blue things are rough.
((("something" "is" "quiet" "+") ("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
If something is round then it is blue.
((("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
If something is kind and rough then it is blue.
((("something" "is" "kind" "+") ("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
All smart things are rough.
((("something" "is" "smart" "+")) -> ("something" "is" "rough" "+"))
If something is rough and blue then it is quiet.
((("something" "is" "rough" "+") ("something" "is" "blue" "+")) -> ("something" "is" "quiet" "+"))
If something is quiet then it is blue.
((("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
Charlie is quiet.
True
1
proof
[(triple5)]
("Charlie" "is" "quiet" "+")
triple5
Charlie is not white.
False
1
inv-proof
[(triple6)]
("Charlie" "is" "white" "-")
triple6
Bob is not kind.
Unknown
inv-random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
@0: Anne is blue.[(triple1)] Anne is rough.[(triple2)] Bob is quiet.[(triple3)] Bob is smart.[(triple4)] Charlie is quiet.[(triple5)] Charlie is white.[(triple6)] Gary is quiet.[(triple7)] Gary is rough.[(triple8 OR ((triple9) -> rule6) OR ((triple7 ((triple7) -> rule8)) -> rule3) OR ((triple7 ((((triple7) -> rule1)) -> rule4)) -> rule3))] Gary is smart.[(triple9)] Gary is white.[(triple10)] @1: Anne is quiet.[(((triple2 triple1) -> rule7))] Bob is blue.[(((triple3) -> rule8) OR ((((triple3) -> rule1)) -> rule4))] Bob is rough.[(((triple4) -> rule6) OR ((triple3 ((triple3) -> rule8)) -> rule3) OR ((triple3 ((((triple3) -> rule1)) -> rule4)) -> rule3))] Bob is round.[(((triple3) -> rule1))] Charlie is blue.[(((triple5) -> rule8) OR ((((triple5) -> rule1)) -> rule4))] Charlie is round.[(((triple5) -> rule1))] Gary is blue.[(((triple7) -> rule8) OR ((((triple7) -> rule1)) -> rule4))] Gary is round.[(((triple7) -> rule1))] @2: Anne is round.[(((((triple2 triple1) -> rule7)) -> rule1))] Charlie is rough.[(((triple5 ((triple5) -> rule8)) -> rule3) OR ((triple5 ((((triple5) -> rule1)) -> rule4)) -> rule3))] @3: Charlie is smart.[(((((triple5 ((triple5) -> rule8)) -> rule3) triple6) -> rule2) OR ((((triple5 ((((triple5) -> rule1)) -> rule4)) -> rule3) triple6) -> rule2))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is rough.
("Anne" "is" "rough" "+")
triple2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
Bob is smart.
("Bob" "is" "smart" "+")
triple4
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple5
Charlie is white.
("Charlie" "is" "white" "+")
triple6
Gary is quiet.
("Gary" "is" "quiet" "+")
triple7
Gary is rough.
("Gary" "is" "rough" "+")
triple8
((triple9) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((triple7 ((triple7) -> (rule8 % int2))) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((triple7 ((((triple7) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
triple9
Gary is white.
("Gary" "is" "white" "+")
triple10
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple2 triple1) -> (rule7 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((triple3) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
((triple4) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((triple3 ((triple3) -> (rule8 % int2))) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((triple3 ((((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
((triple3) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple5) -> (rule8 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((((triple5) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
((triple5) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
((triple7) -> (rule8 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((((triple7) -> (rule1 % int2))) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
((triple7) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
((((triple2 triple1) -> (rule7 % int2))) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple5 ((triple5) -> (rule8 % int2))) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
((triple5 ((((triple5) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
((((triple5 ((triple5) -> (rule8 % int3))) -> (rule3 % int2)) triple6) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
((((triple5 ((((triple5) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule3 % int2)) triple6) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
int4