Dave is big. Dave is quiet. Erin is blue. Erin is nice. Erin is red. Erin is white. Erin is young. Harry is big. Harry is blue. Harry is nice. Harry is quiet. Harry is white. Big things are young. All blue things are red. All white things are quiet. If something is big then it is red. If Harry is white then Harry is young. If something is big and blue then it is red. Quiet, big things are young. If Harry is nice and Harry is red then Harry is big.
Dave is big.
("Dave" "is" "big" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is white.
("Harry" "is" "white" "+")
Big things are young.
((("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
All blue things are red.
((("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
All white things are quiet.
((("something" "is" "white" "+")) -> ("something" "is" "quiet" "+"))
If something is big then it is red.
((("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
If Harry is white then Harry is young.
((("Harry" "is" "white" "+")) -> ("Harry" "is" "young" "+"))
If something is big and blue then it is red.
((("something" "is" "big" "+") ("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
Quiet, big things are young.
((("something" "is" "quiet" "+") ("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
If Harry is nice and Harry is red then Harry is big.
((("Harry" "is" "nice" "+") ("Harry" "is" "red" "+")) -> ("Harry" "is" "big" "+"))
Harry is quiet.
True
1
proof
[(triple11 OR ((triple12) -> rule3))]
("Harry" "is" "quiet" "+")
triple11
((triple12) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is not nice.
False
1
inv-proof
[(triple10)]
("Harry" "is" "nice" "-")
triple10
Harry is red.
True
2
proof
[(((triple8) -> rule4) OR ((triple9) -> rule2) OR ((triple8 triple9) -> rule6))]
("Harry" "is" "red" "+")
((triple8) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((triple9) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((triple8 triple9) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Dave is not young.
False
2
inv-proof
[(((triple1) -> rule1) OR ((triple2 triple1) -> rule7))]
("Dave" "is" "young" "-")
((triple1) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((triple2 triple1) -> (rule7 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Erin is not big.
Unknown
inv-random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
Dave is not blue.
Unknown
inv-random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Dave is big.[(triple1)] Dave is quiet.[(triple2)] Erin is blue.[(triple3)] Erin is nice.[(triple4)] Erin is red.[(triple5 OR ((triple3) -> rule2))] Erin is white.[(triple6)] Erin is young.[(triple7)] Harry is big.[(triple8 OR ((triple10 ((triple9) -> rule2)) -> rule8))] Harry is blue.[(triple9)] Harry is nice.[(triple10)] Harry is quiet.[(triple11 OR ((triple12) -> rule3))] Harry is white.[(triple12)] @1: Dave is red.[(((triple1) -> rule4))] Dave is young.[(((triple1) -> rule1) OR ((triple2 triple1) -> rule7))] Erin is quiet.[(((triple6) -> rule3))] Harry is red.[(((triple8) -> rule4) OR ((triple9) -> rule2) OR ((triple8 triple9) -> rule6))] Harry is young.[(((triple12) -> rule5) OR ((triple8) -> rule1) OR ((triple11 triple8) -> rule7) OR ((((triple12) -> rule3) triple8) -> rule7) OR ((((triple10 ((triple9) -> rule2)) -> rule8)) -> rule1) OR ((triple11 ((triple10 ((triple9) -> rule2)) -> rule8)) -> rule7) OR ((((triple12) -> rule3) ((triple10 ((triple9) -> rule2)) -> rule8)) -> rule7))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple2
Erin is blue.
("Erin" "is" "blue" "+")
triple3
Erin is nice.
("Erin" "is" "nice" "+")
triple4
Erin is red.
("Erin" "is" "red" "+")
triple5
((triple3) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
triple6
Erin is young.
("Erin" "is" "young" "+")
triple7
Harry is big.
("Harry" "is" "big" "+")
triple8
((triple10 ((triple9) -> (rule2 % int2))) -> (rule8 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
triple9
Harry is nice.
("Harry" "is" "nice" "+")
triple10
Harry is quiet.
("Harry" "is" "quiet" "+")
triple11
((triple12) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
triple12
Dave is red.
("Dave" "is" "red" "+")
((triple1) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((triple1) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((triple2 triple1) -> (rule7 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple6) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple8) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((triple9) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((triple8 triple9) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple12) -> (rule5 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((triple8) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((triple11 triple8) -> (rule7 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((((triple12) -> (rule3 % int2)) triple8) -> (rule7 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((triple10 ((triple9) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
((triple11 ((triple10 ((triple9) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
((((triple12) -> (rule3 % int4)) ((triple10 ((triple9) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
int4