Bob is green. Bob is quiet. Bob is round. Bob is young. Charlie is big. Charlie is green. Charlie is kind. Charlie is young. Erin is green. Fiona is big. Fiona is blue. Fiona is green. Fiona is kind. Fiona is quiet. Fiona is round. Fiona is young. Big things are kind. If something is green and blue then it is young. If Erin is blue and Erin is young then Erin is big. All green things are blue. If something is kind and big then it is round. All kind things are big. All quiet, blue things are green. If something is round then it is big.
Bob is green.
("Bob" "is" "green" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Erin is green.
("Erin" "is" "green" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Big things are kind.
((("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
If something is green and blue then it is young.
((("something" "is" "green" "+") ("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
If Erin is blue and Erin is young then Erin is big.
((("Erin" "is" "blue" "+") ("Erin" "is" "young" "+")) -> ("Erin" "is" "big" "+"))
All green things are blue.
((("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
If something is kind and big then it is round.
((("something" "is" "kind" "+") ("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
All kind things are big.
((("something" "is" "kind" "+")) -> ("something" "is" "big" "+"))
All quiet, blue things are green.
((("something" "is" "quiet" "+") ("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
If something is round then it is big.
((("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
Charlie is big.
True
1
proof
[(triple5 OR ((triple7) -> rule6))]
("Charlie" "is" "big" "+")
triple5
((triple7) -> (rule6 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Bob is not quiet.
False
1
inv-proof
[(triple2)]
("Bob" "is" "quiet" "-")
triple2
Bob is blue.
True
2
proof
[(((triple1) -> rule4))]
("Bob" "is" "blue" "+")
((triple1) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Charlie is not blue.
False
2
inv-proof
[(((triple6) -> rule4))]
("Charlie" "is" "blue" "-")
((triple6) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Bob is kind.
True
3
proof
[(((((triple3) -> rule8)) -> rule1))]
("Bob" "is" "kind" "+")
((((triple3) -> (rule8 % int2))) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Erin is not young.
False
4
inv-proof
[(((triple9 ((triple9) -> rule4)) -> rule2))]
("Erin" "is" "young" "-")
((triple9 ((triple9) -> (rule4 % int2))) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is big.
True
7
proof
[(((((triple9) -> rule4) ((triple9 ((triple9) -> rule4)) -> rule2)) -> rule3))]
("Erin" "is" "big" "+")
((((triple9) -> (rule4 % int3)) ((triple9 ((triple9) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is not big.
False
7
inv-proof
[(((((triple9) -> rule4) ((triple9 ((triple9) -> rule4)) -> rule2)) -> rule3))]
("Erin" "is" "big" "-")
((((triple9) -> (rule4 % int3)) ((triple9 ((triple9) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is kind.
True
8
proof
[(((((((triple9) -> rule4) ((triple9 ((triple9) -> rule4)) -> rule2)) -> rule3)) -> rule1))]
("Erin" "is" "kind" "+")
((((((triple9) -> (rule4 % int4)) ((triple9 ((triple9) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is blue.
("Erin" "is" "blue" "+")
int4
Erin is not kind.
False
8
inv-proof
[(((((((triple9) -> rule4) ((triple9 ((triple9) -> rule4)) -> rule2)) -> rule3)) -> rule1))]
("Erin" "is" "kind" "-")
((((((triple9) -> (rule4 % int4)) ((triple9 ((triple9) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is blue.
("Erin" "is" "blue" "+")
int4
Erin is round.
True
16
proof
[(((((((((triple9) -> rule4) ((triple9 ((triple9) -> rule4)) -> rule2)) -> rule3)) -> rule1) ((((triple9) -> rule4) ((triple9 ((triple9) -> rule4)) -> rule2)) -> rule3)) -> rule5))]
("Erin" "is" "round" "+")
((((((((triple9) -> (rule4 % int5)) ((triple9 ((triple9) -> (rule4 % int5))) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule1 % int2)) ((((triple9) -> (rule4 % int5)) ((triple9 ((triple9) -> (rule4 % int5))) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
int4
Erin is blue.
("Erin" "is" "blue" "+")
int5
Erin is not round.
False
16
inv-proof
[(((((((((triple9) -> rule4) ((triple9 ((triple9) -> rule4)) -> rule2)) -> rule3)) -> rule1) ((((triple9) -> rule4) ((triple9 ((triple9) -> rule4)) -> rule2)) -> rule3)) -> rule5))]
("Erin" "is" "round" "-")
((((((((triple9) -> (rule4 % int5)) ((triple9 ((triple9) -> (rule4 % int5))) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule1 % int2)) ((((triple9) -> (rule4 % int5)) ((triple9 ((triple9) -> (rule4 % int5))) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
int4
Erin is blue.
("Erin" "is" "blue" "+")
int5
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Erin is quiet.
Unknown
random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "+")
@0: Bob is green.[(triple1)] Bob is quiet.[(triple2)] Bob is round.[(triple3)] Bob is young.[(triple4 OR ((triple1 ((triple1) -> rule4)) -> rule2))] Charlie is big.[(triple5 OR ((triple7) -> rule6))] Charlie is green.[(triple6)] Charlie is kind.[(triple7 OR ((triple5) -> rule1))] Charlie is young.[(triple8 OR ((triple6 ((triple6) -> rule4)) -> rule2))] Erin is green.[(triple9)] Fiona is big.[(triple10 OR ((triple13) -> rule6) OR ((triple15) -> rule8))] Fiona is blue.[(triple11 OR ((triple12) -> rule4))] Fiona is green.[(triple12 OR ((triple14 triple11) -> rule7))] Fiona is kind.[(triple13 OR ((triple10) -> rule1) OR ((((triple15) -> rule8)) -> rule1))] Fiona is quiet.[(triple14)] Fiona is round.[(triple15 OR ((triple13 triple10) -> rule5) OR ((triple13 ((triple13) -> rule6)) -> rule5) OR ((((triple10) -> rule1) triple10) -> rule5) OR ((((triple10) -> rule1) ((triple13) -> rule6)) -> rule5))] Fiona is young.[(triple16 OR ((triple12 triple11) -> rule2) OR ((triple12 ((triple12) -> rule4)) -> rule2) OR ((((triple14 triple11) -> rule7) triple11) -> rule2) OR ((((triple14 triple11) -> rule7) ((triple12) -> rule4)) -> rule2))] @1: Bob is big.[(((triple3) -> rule8))] Bob is blue.[(((triple1) -> rule4))] Charlie is blue.[(((triple6) -> rule4))] Charlie is round.[(((triple7 triple5) -> rule5) OR ((triple7 ((triple7) -> rule6)) -> rule5) OR ((((triple5) -> rule1) triple5) -> rule5) OR ((((triple5) -> rule1) ((triple7) -> rule6)) -> rule5))] Erin is blue.[(((triple9) -> rule4))] @2: Bob is kind.[(((((triple3) -> rule8)) -> rule1))] Erin is young.[(((triple9 ((triple9) -> rule4)) -> rule2))] @3: Erin is big.[(((((triple9) -> rule4) ((triple9 ((triple9) -> rule4)) -> rule2)) -> rule3))] @4: Erin is kind.[(((((((triple9) -> rule4) ((triple9 ((triple9) -> rule4)) -> rule2)) -> rule3)) -> rule1))] @5: Erin is round.[(((((((((triple9) -> rule4) ((triple9 ((triple9) -> rule4)) -> rule2)) -> rule3)) -> rule1) ((((triple9) -> rule4) ((triple9 ((triple9) -> rule4)) -> rule2)) -> rule3)) -> rule5))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
Bob is round.
("Bob" "is" "round" "+")
triple3
Bob is young.
("Bob" "is" "young" "+")
triple4
((triple1 ((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
triple5
((triple7) -> (rule6 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
triple6
Charlie is kind.
("Charlie" "is" "kind" "+")
triple7
((triple5) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
triple8
((triple6 ((triple6) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
triple9
Fiona is big.
("Fiona" "is" "big" "+")
triple10
((triple13) -> (rule6 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
((triple15) -> (rule8 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
triple11
((triple12) -> (rule4 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
triple12
((triple14 triple11) -> (rule7 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
triple13
((triple10) -> (rule1 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
((((triple15) -> (rule8 % int2))) -> (rule1 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple14
Fiona is round.
("Fiona" "is" "round" "+")
triple15
((triple13 triple10) -> (rule5 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
((triple13 ((triple13) -> (rule6 % int2))) -> (rule5 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
((((triple10) -> (rule1 % int2)) triple10) -> (rule5 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
((((triple10) -> (rule1 % int3)) ((triple13) -> (rule6 % int2))) -> (rule5 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is young.
("Fiona" "is" "young" "+")
triple16
((triple12 triple11) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
((triple12 ((triple12) -> (rule4 % int2))) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
((((triple14 triple11) -> (rule7 % int2)) triple11) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
((((triple14 triple11) -> (rule7 % int3)) ((triple12) -> (rule4 % int2))) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
((triple3) -> (rule8 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((triple1) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple6) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((triple7 triple5) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((triple7 ((triple7) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((((triple5) -> (rule1 % int2)) triple5) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((triple5) -> (rule1 % int3)) ((triple7) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Erin is blue.
("Erin" "is" "blue" "+")
((triple9) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((((triple3) -> (rule8 % int2))) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
((triple9 ((triple9) -> (rule4 % int2))) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
((((triple9) -> (rule4 % int3)) ((triple9 ((triple9) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
((((((triple9) -> (rule4 % int4)) ((triple9 ((triple9) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is blue.
("Erin" "is" "blue" "+")
int4
Erin is round.
("Erin" "is" "round" "+")
((((((((triple9) -> (rule4 % int5)) ((triple9 ((triple9) -> (rule4 % int5))) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule1 % int2)) ((((triple9) -> (rule4 % int5)) ((triple9 ((triple9) -> (rule4 % int5))) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
int4
Erin is blue.
("Erin" "is" "blue" "+")
int5