Anne is big. Anne is blue. Anne is quiet. Anne is smart. Charlie is blue. Charlie is green. Dave is green. If someone is big then they are green. All rough, green people are big. If someone is smart then they are blue. All blue, quiet people are big. Green people are smart. If someone is smart and green then they are quiet.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Dave is green.
("Dave" "is" "green" "+")
If someone is big then they are green.
((("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
All rough, green people are big.
((("someone" "is" "rough" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "big" "+"))
If someone is smart then they are blue.
((("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "+"))
All blue, quiet people are big.
((("someone" "is" "blue" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "+"))
Green people are smart.
((("someone" "is" "green" "+")) -> ("someone" "is" "smart" "+"))
If someone is smart and green then they are quiet.
((("someone" "is" "smart" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "quiet" "+"))
Charlie is blue.
True
1
proof
[(triple5 OR ((((triple6) -> rule5)) -> rule3))]
("Charlie" "is" "blue" "+")
triple5
((((triple6) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Dave is not green.
False
1
inv-proof
[(triple7)]
("Dave" "is" "green" "-")
triple7
Charlie is not young.
Unknown
inv-random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
@0: Anne is big.[(triple1 OR ((triple2 triple3) -> rule4) OR ((((triple4) -> rule3) triple3) -> rule4))] Anne is blue.[(triple2 OR ((triple4) -> rule3) OR ((((((triple1) -> rule1)) -> rule5)) -> rule3))] Anne is quiet.[(triple3 OR ((triple4 ((triple1) -> rule1)) -> rule6) OR ((((((triple1) -> rule1)) -> rule5) ((triple1) -> rule1)) -> rule6))] Anne is smart.[(triple4 OR ((((triple1) -> rule1)) -> rule5) OR ((((((triple2 triple3) -> rule4)) -> rule1)) -> rule5))] Charlie is blue.[(triple5 OR ((((triple6) -> rule5)) -> rule3))] Charlie is green.[(triple6)] Dave is green.[(triple7)] @1: Anne is green.[(((triple1) -> rule1) OR ((((triple2 triple3) -> rule4)) -> rule1) OR ((((((triple4) -> rule3) triple3) -> rule4)) -> rule1))] Charlie is smart.[(((triple6) -> rule5))] Dave is smart.[(((triple7) -> rule5))] @2: Charlie is quiet.[(((((triple6) -> rule5) triple6) -> rule6))] Dave is blue.[(((((triple7) -> rule5)) -> rule3))] Dave is quiet.[(((((triple7) -> rule5) triple7) -> rule6))] @3: Charlie is big.[(((triple5 ((((triple6) -> rule5) triple6) -> rule6)) -> rule4) OR ((((((triple6) -> rule5)) -> rule3) ((((triple6) -> rule5) triple6) -> rule6)) -> rule4))] Dave is big.[(((((((triple7) -> rule5)) -> rule3) ((((triple7) -> rule5) triple7) -> rule6)) -> rule4))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple2 triple3) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((((triple4) -> (rule3 % int2)) triple3) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
triple2
((triple4) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
((triple4 ((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
((((((triple1) -> (rule1 % int3))) -> (rule5 % int2)) ((triple1) -> (rule1 % int3))) -> (rule6 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
triple4
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
((((((triple2 triple3) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Charlie is blue.
("Charlie" "is" "blue" "+")
triple5
((((triple6) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
triple6
Dave is green.
("Dave" "is" "green" "+")
triple7
Anne is green.
("Anne" "is" "green" "+")
((triple1) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((((triple2 triple3) -> (rule4 % int2))) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
((((((triple4) -> (rule3 % int3)) triple3) -> (rule4 % int2))) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple6) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple7) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((triple6) -> (rule5 % int2)) triple6) -> (rule6 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
((((triple7) -> (rule5 % int2))) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
((((triple7) -> (rule5 % int2)) triple7) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
((triple5 ((((triple6) -> (rule5 % int3)) triple6) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
((((((triple6) -> (rule5 % int4))) -> (rule3 % int3)) ((((triple6) -> (rule5 % int4)) triple6) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
int4
Dave is big.
("Dave" "is" "big" "+")
((((((triple7) -> (rule5 % int4))) -> (rule3 % int3)) ((((triple7) -> (rule5 % int4)) triple7) -> (rule6 % int2))) -> (rule4 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
int4