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