Anne is smart. Anne is young. Bob is quiet. If someone is smart then they are white. All round, smart people are young. All smart people are big. If Bob is smart and Bob is quiet then Bob is white. If someone is green and young then they are big. If someone is young then they are smart. White people are green. If someone is quiet then they are young.
Anne is smart.
("Anne" "is" "smart" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
If someone is smart then they are white.
((("someone" "is" "smart" "+")) -> ("someone" "is" "white" "+"))
All round, smart people are young.
((("someone" "is" "round" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "young" "+"))
All smart people are big.
((("someone" "is" "smart" "+")) -> ("someone" "is" "big" "+"))
If Bob is smart and Bob is quiet then Bob is white.
((("Bob" "is" "smart" "+") ("Bob" "is" "quiet" "+")) -> ("Bob" "is" "white" "+"))
If someone is green and young then they are big.
((("someone" "is" "green" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "big" "+"))
If someone is young then they are smart.
((("someone" "is" "young" "+")) -> ("someone" "is" "smart" "+"))
White people are green.
((("someone" "is" "white" "+")) -> ("someone" "is" "green" "+"))
If someone is quiet then they are young.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "young" "+"))
Anne is young.
True
1
proof
[(triple2)]
("Anne" "is" "young" "+")
triple2
Anne is not young.
False
1
inv-proof
[(triple2)]
("Anne" "is" "young" "-")
triple2
Bob is young.
True
2
proof
[(((triple3) -> rule8))]
("Bob" "is" "young" "+")
((triple3) -> (rule8 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Anne is not big.
False
2
inv-proof
[(((triple1) -> rule3) OR ((((triple2) -> rule6)) -> rule3) OR ((((((triple1) -> rule1)) -> rule7) triple2) -> rule5) OR ((((((((triple2) -> rule6)) -> rule1)) -> rule7) triple2) -> rule5))]
("Anne" "is" "big" "-")
((triple1) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
((((((triple1) -> (rule1 % int3))) -> (rule7 % int2)) triple2) -> (rule5 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
((((((((triple2) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule7 % int2)) triple2) -> (rule5 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4
Bob is smart.
True
3
proof
[(((((triple3) -> rule8)) -> rule6))]
("Bob" "is" "smart" "+")
((((triple3) -> (rule8 % int2))) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Anne is not green.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule7) OR ((((((triple2) -> rule6)) -> rule1)) -> rule7))]
("Anne" "is" "green" "-")
((((triple1) -> (rule1 % int2))) -> (rule7 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
((((((triple2) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Bob is big.
True
4
proof
[(((((((triple3) -> rule8)) -> rule6)) -> rule3) OR ((((((((((triple3) -> rule8)) -> rule6)) -> rule1)) -> rule7) ((triple3) -> rule8)) -> rule5) OR ((((((((((triple3) -> rule8)) -> rule6) triple3) -> rule4)) -> rule7) ((triple3) -> rule8)) -> rule5))]
("Bob" "is" "big" "+")
((((((triple3) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
((((((((((triple3) -> (rule8 % int5))) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule7 % int2)) ((triple3) -> (rule8 % int5))) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
Bob is young.
("Bob" "is" "young" "+")
int5
((((((((((triple3) -> (rule8 % int5))) -> (rule6 % int4)) triple3) -> (rule4 % int3))) -> (rule7 % int2)) ((triple3) -> (rule8 % int5))) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
Bob is young.
("Bob" "is" "young" "+")
int5
Bob is not white.
False
4
inv-proof
[(((((((triple3) -> rule8)) -> rule6)) -> rule1) OR ((((((triple3) -> rule8)) -> rule6) triple3) -> rule4))]
("Bob" "is" "white" "-")
((((((triple3) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
((((((triple3) -> (rule8 % int3))) -> (rule6 % int2)) triple3) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Anne is not round.
Unknown
inv-random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "-")
Anne is quiet.
Unknown
random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "+")
@0: Anne is smart.[(triple1 OR ((triple2) -> rule6))] Anne is young.[(triple2)] Bob is quiet.[(triple3)] @1: Anne is big.[(((triple1) -> rule3) OR ((((triple2) -> rule6)) -> rule3) OR ((((((triple1) -> rule1)) -> rule7) triple2) -> rule5) OR ((((((((triple2) -> rule6)) -> rule1)) -> rule7) triple2) -> rule5))] Anne is white.[(((triple1) -> rule1) OR ((((triple2) -> rule6)) -> rule1))] Bob is young.[(((triple3) -> rule8))] @2: Anne is green.[(((((triple1) -> rule1)) -> rule7) OR ((((((triple2) -> rule6)) -> rule1)) -> rule7))] Bob is smart.[(((((triple3) -> rule8)) -> rule6))] @3: Bob is big.[(((((((triple3) -> rule8)) -> rule6)) -> rule3) OR ((((((((((triple3) -> rule8)) -> rule6)) -> rule1)) -> rule7) ((triple3) -> rule8)) -> rule5) OR ((((((((((triple3) -> rule8)) -> rule6) triple3) -> rule4)) -> rule7) ((triple3) -> rule8)) -> rule5))] Bob is white.[(((((((triple3) -> rule8)) -> rule6)) -> rule1) OR ((((((triple3) -> rule8)) -> rule6) triple3) -> rule4))] @4: Bob is green.[(((((((((triple3) -> rule8)) -> rule6)) -> rule1)) -> rule7) OR ((((((((triple3) -> rule8)) -> rule6) triple3) -> rule4)) -> rule7))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
((triple2) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
triple2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
Anne is big.
("Anne" "is" "big" "+")
((triple1) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
((((((triple1) -> (rule1 % int3))) -> (rule7 % int2)) triple2) -> (rule5 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
((((((((triple2) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule7 % int2)) triple2) -> (rule5 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4
Anne is white.
("Anne" "is" "white" "+")
((triple1) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((((triple2) -> (rule6 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
((triple3) -> (rule8 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
((((triple1) -> (rule1 % int2))) -> (rule7 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
((((((triple2) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
((((triple3) -> (rule8 % int2))) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
((((((triple3) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
((((((((((triple3) -> (rule8 % int5))) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule7 % int2)) ((triple3) -> (rule8 % int5))) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
Bob is young.
("Bob" "is" "young" "+")
int5
((((((((((triple3) -> (rule8 % int5))) -> (rule6 % int4)) triple3) -> (rule4 % int3))) -> (rule7 % int2)) ((triple3) -> (rule8 % int5))) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
Bob is young.
("Bob" "is" "young" "+")
int5
Bob is white.
("Bob" "is" "white" "+")
((((((triple3) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
((((((triple3) -> (rule8 % int3))) -> (rule6 % int2)) triple3) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
((((((((triple3) -> (rule8 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4
((((((((triple3) -> (rule8 % int4))) -> (rule6 % int3)) triple3) -> (rule4 % int2))) -> (rule7 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4