Dave is big. Dave is furry. Dave is quiet. Dave is red. Dave is smart. Dave is white. Fiona is big. Fiona is furry. Fiona is red. Fiona is round. Fiona is smart. Fiona is white. Harry is quiet. Harry is red. Harry is smart. All quiet things are round. Round things are white. White things are round. If something is furry and quiet then it is smart. If something is red and white then it is furry. If something is big and furry then it is white. If Fiona is smart then Fiona is furry. If Harry is furry and Harry is big then Harry is red.
Dave is big.
("Dave" "is" "big" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
All quiet things are round.
((("something" "is" "quiet" "+")) -> ("something" "is" "round" "+"))
Round things are white.
((("something" "is" "round" "+")) -> ("something" "is" "white" "+"))
White things are round.
((("something" "is" "white" "+")) -> ("something" "is" "round" "+"))
If something is furry and quiet then it is smart.
((("something" "is" "furry" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "smart" "+"))
If something is red and white then it is furry.
((("something" "is" "red" "+") ("something" "is" "white" "+")) -> ("something" "is" "furry" "+"))
If something is big and furry then it is white.
((("something" "is" "big" "+") ("something" "is" "furry" "+")) -> ("something" "is" "white" "+"))
If Fiona is smart then Fiona is furry.
((("Fiona" "is" "smart" "+")) -> ("Fiona" "is" "furry" "+"))
If Harry is furry and Harry is big then Harry is red.
((("Harry" "is" "furry" "+") ("Harry" "is" "big" "+")) -> ("Harry" "is" "red" "+"))
Harry is smart.
True
1
proof
[(triple15 OR ((((triple14 ((((triple13) -> rule1)) -> rule2)) -> rule5) triple13) -> rule4))]
("Harry" "is" "smart" "+")
triple15
((((triple14 ((((triple13) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule5 % int2)) triple13) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
int4
Fiona is not furry.
False
1
inv-proof
[(triple8 OR ((triple11) -> rule7) OR ((triple9 triple12) -> rule5) OR ((triple9 ((triple10) -> rule2)) -> rule5))]
("Fiona" "is" "furry" "-")
triple8
((triple11) -> (rule7 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
((triple9 triple12) -> (rule5 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
((triple9 ((triple10) -> (rule2 % int2))) -> (rule5 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Dave is round.
True
2
proof
[(((triple3) -> rule1) OR ((triple6) -> rule3) OR ((((triple1 triple2) -> rule6)) -> rule3))]
("Dave" "is" "round" "+")
((triple3) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((triple6) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((((triple1 triple2) -> (rule6 % int2))) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is not round.
False
2
inv-proof
[(((triple3) -> rule1) OR ((triple6) -> rule3) OR ((((triple1 triple2) -> rule6)) -> rule3))]
("Dave" "is" "round" "-")
((triple3) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((triple6) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((((triple1 triple2) -> (rule6 % int2))) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Harry is white.
True
3
proof
[(((((triple13) -> rule1)) -> rule2))]
("Harry" "is" "white" "+")
((((triple13) -> (rule1 % int2))) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is not white.
False
3
inv-proof
[(((((triple13) -> rule1)) -> rule2))]
("Harry" "is" "white" "-")
((((triple13) -> (rule1 % int2))) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is furry.
True
5
proof
[(((triple14 ((((triple13) -> rule1)) -> rule2)) -> rule5))]
("Harry" "is" "furry" "+")
((triple14 ((((triple13) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is not furry.
False
5
inv-proof
[(((triple14 ((((triple13) -> rule1)) -> rule2)) -> rule5))]
("Harry" "is" "furry" "-")
((triple14 ((((triple13) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is not big.
Unknown
inv-random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
@0: Dave is big.[(triple1)] Dave is furry.[(triple2 OR ((triple4 triple6) -> rule5) OR ((triple4 ((((triple3) -> rule1)) -> rule2)) -> rule5))] Dave is quiet.[(triple3)] Dave is red.[(triple4)] Dave is smart.[(triple5 OR ((triple2 triple3) -> rule4) OR ((((triple4 triple6) -> rule5) triple3) -> rule4) OR ((((triple4 ((((triple3) -> rule1)) -> rule2)) -> rule5) triple3) -> rule4))] Dave is white.[(triple6 OR ((triple1 triple2) -> rule6) OR ((((triple3) -> rule1)) -> rule2))] Fiona is big.[(triple7)] Fiona is furry.[(triple8 OR ((triple11) -> rule7) OR ((triple9 triple12) -> rule5) OR ((triple9 ((triple10) -> rule2)) -> rule5))] Fiona is red.[(triple9)] Fiona is round.[(triple10 OR ((triple12) -> rule3) OR ((((triple7 triple8) -> rule6)) -> rule3) OR ((((triple7 ((triple11) -> rule7)) -> rule6)) -> rule3))] Fiona is smart.[(triple11)] Fiona is white.[(triple12 OR ((triple10) -> rule2) OR ((triple7 triple8) -> rule6) OR ((triple7 ((triple11) -> rule7)) -> rule6))] Harry is quiet.[(triple13)] Harry is red.[(triple14)] Harry is smart.[(triple15 OR ((((triple14 ((((triple13) -> rule1)) -> rule2)) -> rule5) triple13) -> rule4))] @1: Dave is round.[(((triple3) -> rule1) OR ((triple6) -> rule3) OR ((((triple1 triple2) -> rule6)) -> rule3))] Harry is round.[(((triple13) -> rule1))] @2: Harry is white.[(((((triple13) -> rule1)) -> rule2))] @3: Harry is furry.[(((triple14 ((((triple13) -> rule1)) -> rule2)) -> rule5))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
((triple4 triple6) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((triple4 ((((triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
triple3
Dave is red.
("Dave" "is" "red" "+")
triple4
Dave is smart.
("Dave" "is" "smart" "+")
triple5
((triple2 triple3) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((((triple4 triple6) -> (rule5 % int2)) triple3) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
((((triple4 ((((triple3) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule5 % int2)) triple3) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
Dave is white.
("Dave" "is" "white" "+")
triple6
((triple1 triple2) -> (rule6 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
triple7
Fiona is furry.
("Fiona" "is" "furry" "+")
triple8
((triple11) -> (rule7 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
((triple9 triple12) -> (rule5 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
((triple9 ((triple10) -> (rule2 % int2))) -> (rule5 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
triple9
Fiona is round.
("Fiona" "is" "round" "+")
triple10
((triple12) -> (rule3 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
((((triple7 triple8) -> (rule6 % int2))) -> (rule3 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
((((triple7 ((triple11) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
triple11
Fiona is white.
("Fiona" "is" "white" "+")
triple12
((triple10) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
((triple7 triple8) -> (rule6 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
((triple7 ((triple11) -> (rule7 % int2))) -> (rule6 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
triple13
Harry is red.
("Harry" "is" "red" "+")
triple14
Harry is smart.
("Harry" "is" "smart" "+")
triple15
((((triple14 ((((triple13) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule5 % int2)) triple13) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
int4
Dave is round.
("Dave" "is" "round" "+")
((triple3) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((triple6) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((((triple1 triple2) -> (rule6 % int2))) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
((triple13) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((((triple13) -> (rule1 % int2))) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
((triple14 ((((triple13) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3