Dave is blue. Dave is nice. Dave is smart. Erin is big. Erin is blue. Erin is quiet. Erin is rough. Erin is white. Fiona is blue. Harry is big. Harry is blue. Harry is nice. Harry is quiet. Harry is smart. Harry is white. All white, blue people are quiet. If someone is quiet and white then they are big. Blue people are white. If someone is big then they are white. Nice people are white. If Fiona is blue then Fiona is big. If someone is quiet and rough then they are white. If someone is rough and white then they are big.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is white.
("Erin" "is" "white" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
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 smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
All white, blue people are quiet.
((("someone" "is" "white" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "+"))
If someone is quiet and white then they are big.
((("someone" "is" "quiet" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
Blue people are white.
((("someone" "is" "blue" "+")) -> ("someone" "is" "white" "+"))
If someone is big then they are white.
((("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
Nice people are white.
((("someone" "is" "nice" "+")) -> ("someone" "is" "white" "+"))
If Fiona is blue then Fiona is big.
((("Fiona" "is" "blue" "+")) -> ("Fiona" "is" "big" "+"))
If someone is quiet and rough then they are white.
((("someone" "is" "quiet" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "white" "+"))
If someone is rough and white then they are big.
((("someone" "is" "rough" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
Erin is white.
True
1
proof
[(triple8 OR ((triple4) -> rule4) OR ((triple5) -> rule3) OR ((triple6 triple7) -> rule7))]
("Erin" "is" "white" "+")
triple8
((triple4) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((triple5) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((triple6 triple7) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Dave is not blue.
False
1
inv-proof
[(triple1)]
("Dave" "is" "blue" "-")
triple1
Fiona is white.
True
2
proof
[(((triple9) -> rule3) OR ((((triple9) -> rule6)) -> rule4))]
("Fiona" "is" "white" "+")
((triple9) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
((((triple9) -> (rule6 % int2))) -> (rule4 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is not white.
False
2
inv-proof
[(((triple9) -> rule3) OR ((((triple9) -> rule6)) -> rule4))]
("Fiona" "is" "white" "-")
((triple9) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
((((triple9) -> (rule6 % int2))) -> (rule4 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is quiet.
True
4
proof
[(((((triple9) -> rule3) triple9) -> rule1) OR ((((((triple9) -> rule6)) -> rule4) triple9) -> rule1))]
("Fiona" "is" "quiet" "+")
((((triple9) -> (rule3 % int2)) triple9) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
((((((triple9) -> (rule6 % int3))) -> (rule4 % int2)) triple9) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Dave is not quiet.
False
4
inv-proof
[(((((triple1) -> rule3) triple1) -> rule1) OR ((((triple2) -> rule5) triple1) -> rule1))]
("Dave" "is" "quiet" "-")
((((triple1) -> (rule3 % int2)) triple1) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((triple2) -> (rule5 % int2)) triple1) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Erin is not smart.
Unknown
inv-random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "-")
Erin is nice.
Unknown
random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "+")
Dave is not rough.
Unknown
inv-random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "-")
Harry is rough.
Unknown
random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "+")
Fiona is not nice.
Unknown
inv-random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "-")
Fiona is smart.
Unknown
random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "+")
@0: Dave is blue.[(triple1)] Dave is nice.[(triple2)] Dave is smart.[(triple3)] Erin is big.[(triple4 OR ((triple6 triple8) -> rule2) OR ((triple7 triple8) -> rule8) OR ((triple6 ((triple5) -> rule3)) -> rule2) OR ((triple6 ((triple6 triple7) -> rule7)) -> rule2) OR ((triple7 ((triple5) -> rule3)) -> rule8) OR ((triple7 ((triple6 triple7) -> rule7)) -> rule8) OR ((((triple8 triple5) -> rule1) triple8) -> rule2) OR ((((triple8 triple5) -> rule1) ((triple5) -> rule3)) -> rule2) OR ((((triple8 triple5) -> rule1) ((triple6 triple7) -> rule7)) -> rule2) OR ((((((triple5) -> rule3) triple5) -> rule1) triple8) -> rule2) OR ((((((triple5) -> rule3) triple5) -> rule1) ((triple5) -> rule3)) -> rule2) OR ((((((triple5) -> rule3) triple5) -> rule1) ((triple6 triple7) -> rule7)) -> rule2))] Erin is blue.[(triple5)] Erin is quiet.[(triple6 OR ((triple8 triple5) -> rule1) OR ((((triple4) -> rule4) triple5) -> rule1) OR ((((triple5) -> rule3) triple5) -> rule1))] Erin is rough.[(triple7)] Erin is white.[(triple8 OR ((triple4) -> rule4) OR ((triple5) -> rule3) OR ((triple6 triple7) -> rule7))] Fiona is blue.[(triple9)] Harry is big.[(triple10 OR ((triple13 triple15) -> rule2) OR ((triple13 ((triple11) -> rule3)) -> rule2) OR ((triple13 ((triple12) -> rule5)) -> rule2) OR ((((triple15 triple11) -> rule1) triple15) -> rule2) OR ((((triple15 triple11) -> rule1) ((triple11) -> rule3)) -> rule2) OR ((((triple15 triple11) -> rule1) ((triple12) -> rule5)) -> rule2) OR ((((((triple11) -> rule3) triple11) -> rule1) triple15) -> rule2) OR ((((((triple12) -> rule5) triple11) -> rule1) triple15) -> rule2) OR ((((((triple11) -> rule3) triple11) -> rule1) ((triple11) -> rule3)) -> rule2) OR ((((((triple11) -> rule3) triple11) -> rule1) ((triple12) -> rule5)) -> rule2) OR ((((((triple12) -> rule5) triple11) -> rule1) ((triple11) -> rule3)) -> rule2) OR ((((((triple12) -> rule5) triple11) -> rule1) ((triple12) -> rule5)) -> rule2))] Harry is blue.[(triple11)] Harry is nice.[(triple12)] Harry is quiet.[(triple13 OR ((triple15 triple11) -> rule1) OR ((((triple10) -> rule4) triple11) -> rule1) OR ((((triple11) -> rule3) triple11) -> rule1) OR ((((triple12) -> rule5) triple11) -> rule1))] Harry is smart.[(triple14)] Harry is white.[(triple15 OR ((triple10) -> rule4) OR ((triple11) -> rule3) OR ((triple12) -> rule5))] @1: Dave is white.[(((triple1) -> rule3) OR ((triple2) -> rule5))] Fiona is big.[(((triple9) -> rule6) OR ((((((triple9) -> rule3) triple9) -> rule1) ((triple9) -> rule3)) -> rule2))] Fiona is white.[(((triple9) -> rule3) OR ((((triple9) -> rule6)) -> rule4))] @2: Dave is quiet.[(((((triple1) -> rule3) triple1) -> rule1) OR ((((triple2) -> rule5) triple1) -> rule1))] Fiona is quiet.[(((((triple9) -> rule3) triple9) -> rule1) OR ((((((triple9) -> rule6)) -> rule4) triple9) -> rule1))] @3: Dave is big.[(((((((triple1) -> rule3) triple1) -> rule1) ((triple1) -> rule3)) -> rule2) OR ((((((triple1) -> rule3) triple1) -> rule1) ((triple2) -> rule5)) -> rule2) OR ((((((triple2) -> rule5) triple1) -> rule1) ((triple1) -> rule3)) -> rule2) OR ((((((triple2) -> rule5) triple1) -> rule1) ((triple2) -> rule5)) -> rule2))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
Dave is nice.
("Dave" "is" "nice" "+")
triple2
Dave is smart.
("Dave" "is" "smart" "+")
triple3
Erin is big.
("Erin" "is" "big" "+")
triple4
((triple6 triple8) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((triple7 triple8) -> (rule8 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((triple6 ((triple5) -> (rule3 % int2))) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((triple6 ((triple6 triple7) -> (rule7 % int2))) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((triple7 ((triple5) -> (rule3 % int2))) -> (rule8 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((triple7 ((triple6 triple7) -> (rule7 % int2))) -> (rule8 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((((triple8 triple5) -> (rule1 % int2)) triple8) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
((((triple8 triple5) -> (rule1 % int3)) ((triple5) -> (rule3 % int2))) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
((((triple8 triple5) -> (rule1 % int3)) ((triple6 triple7) -> (rule7 % int2))) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
((((((triple5) -> (rule3 % int3)) triple5) -> (rule1 % int2)) triple8) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
((((((triple5) -> (rule3 % int3)) triple5) -> (rule1 % int2)) ((triple5) -> (rule3 % int3))) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
((((((triple5) -> (rule3 % int3)) triple5) -> (rule1 % int2)) ((triple6 triple7) -> (rule7 % int3))) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Erin is blue.
("Erin" "is" "blue" "+")
triple5
Erin is quiet.
("Erin" "is" "quiet" "+")
triple6
((triple8 triple5) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((((triple4) -> (rule4 % int2)) triple5) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((((triple5) -> (rule3 % int2)) triple5) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
triple7
Erin is white.
("Erin" "is" "white" "+")
triple8
((triple4) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((triple5) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((triple6 triple7) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
triple9
Harry is big.
("Harry" "is" "big" "+")
triple10
((triple13 triple15) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((triple13 ((triple11) -> (rule3 % int2))) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((triple13 ((triple12) -> (rule5 % int2))) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((((triple15 triple11) -> (rule1 % int2)) triple15) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((triple15 triple11) -> (rule1 % int3)) ((triple11) -> (rule3 % int2))) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
((((triple15 triple11) -> (rule1 % int3)) ((triple12) -> (rule5 % int2))) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
((((((triple11) -> (rule3 % int3)) triple11) -> (rule1 % int2)) triple15) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
((((((triple12) -> (rule5 % int3)) triple11) -> (rule1 % int2)) triple15) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
((((((triple11) -> (rule3 % int3)) triple11) -> (rule1 % int2)) ((triple11) -> (rule3 % int3))) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
((((((triple11) -> (rule3 % int3)) triple11) -> (rule1 % int2)) ((triple12) -> (rule5 % int3))) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
((((((triple12) -> (rule5 % int3)) triple11) -> (rule1 % int2)) ((triple11) -> (rule3 % int3))) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
((((((triple12) -> (rule5 % int3)) triple11) -> (rule1 % int2)) ((triple12) -> (rule5 % int3))) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
triple11
Harry is nice.
("Harry" "is" "nice" "+")
triple12
Harry is quiet.
("Harry" "is" "quiet" "+")
triple13
((triple15 triple11) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((((triple10) -> (rule4 % int2)) triple11) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((((triple11) -> (rule3 % int2)) triple11) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((((triple12) -> (rule5 % int2)) triple11) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
triple14
Harry is white.
("Harry" "is" "white" "+")
triple15
((triple10) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((triple11) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((triple12) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
((triple1) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((triple2) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
((triple9) -> (rule6 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
((((((triple9) -> (rule3 % int3)) triple9) -> (rule1 % int2)) ((triple9) -> (rule3 % int3))) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Fiona is white.
("Fiona" "is" "white" "+")
((triple9) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
((((triple9) -> (rule6 % int2))) -> (rule4 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
((((triple1) -> (rule3 % int2)) triple1) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((triple2) -> (rule5 % int2)) triple1) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((((triple9) -> (rule3 % int2)) triple9) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
((((((triple9) -> (rule6 % int3))) -> (rule4 % int2)) triple9) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
((((((triple1) -> (rule3 % int3)) triple1) -> (rule1 % int2)) ((triple1) -> (rule3 % int3))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
((((((triple1) -> (rule3 % int3)) triple1) -> (rule1 % int2)) ((triple2) -> (rule5 % int3))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
((((((triple2) -> (rule5 % int3)) triple1) -> (rule1 % int2)) ((triple1) -> (rule3 % int3))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
((((((triple2) -> (rule5 % int3)) triple1) -> (rule1 % int2)) ((triple2) -> (rule5 % int3))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3