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