Anne is blue. Anne is quiet. Anne is rough. Anne is round. Dave is blue. Dave is cold. Dave is quiet. Dave is round. Dave is smart. Fiona is cold. Fiona is rough. Harry is cold. Harry is green. Harry is round. Harry is smart. If Anne is round then Anne is green. All cold, rough people are smart. If someone is quiet and smart then they are cold. If someone is quiet then they are blue. Round people are blue. All green people are cold. If Dave is cold and Dave is quiet then Dave is green. Smart people are quiet.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is round.
("Anne" "is" "round" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If Anne is round then Anne is green.
((("Anne" "is" "round" "+")) -> ("Anne" "is" "green" "+"))
All cold, rough people are smart.
((("someone" "is" "cold" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
If someone is quiet and smart then they are cold.
((("someone" "is" "quiet" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "+"))
If someone is quiet then they are blue.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "blue" "+"))
Round people are blue.
((("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
All green people are cold.
((("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
If Dave is cold and Dave is quiet then Dave is green.
((("Dave" "is" "cold" "+") ("Dave" "is" "quiet" "+")) -> ("Dave" "is" "green" "+"))
Smart people are quiet.
((("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
Dave is quiet.
True
1
proof
[(triple7 OR ((triple9) -> rule8))]
("Dave" "is" "quiet" "+")
triple7
((triple9) -> (rule8 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Harry is not cold.
False
1
inv-proof
[(triple12 OR ((triple13) -> rule6) OR ((((triple15) -> rule8) triple15) -> rule3))]
("Harry" "is" "cold" "-")
triple12
((triple13) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((((triple15) -> (rule8 % int2)) triple15) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is blue.
True
2
proof
[(((triple14) -> rule5) OR ((((triple15) -> rule8)) -> rule4))]
("Harry" "is" "blue" "+")
((triple14) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((((triple15) -> (rule8 % int2))) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is not blue.
False
2
inv-proof
[(((triple14) -> rule5) OR ((((triple15) -> rule8)) -> rule4))]
("Harry" "is" "blue" "-")
((triple14) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((((triple15) -> (rule8 % int2))) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Anne is cold.
True
3
proof
[(((((triple4) -> rule1)) -> rule6))]
("Anne" "is" "cold" "+")
((((triple4) -> (rule1 % int2))) -> (rule6 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is not cold.
False
3
inv-proof
[(((((triple4) -> rule1)) -> rule6))]
("Anne" "is" "cold" "-")
((((triple4) -> (rule1 % int2))) -> (rule6 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is smart.
True
5
proof
[(((((((triple4) -> rule1)) -> rule6) triple3) -> rule2))]
("Anne" "is" "smart" "+")
((((((triple4) -> (rule1 % int3))) -> (rule6 % int2)) triple3) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Fiona is not blue.
False
5
inv-proof
[(((((((triple10 triple11) -> rule2)) -> rule8)) -> rule4))]
("Fiona" "is" "blue" "-")
((((((triple10 triple11) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is not round.
Unknown
inv-random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "-")
Fiona is green.
Unknown
random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "+")
Harry is not rough.
Unknown
inv-random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
@0: Anne is blue.[(triple1 OR ((triple2) -> rule4) OR ((triple4) -> rule5) OR ((((((((((triple4) -> rule1)) -> rule6) triple3) -> rule2)) -> rule8)) -> rule4))] Anne is quiet.[(triple2 OR ((((((((triple4) -> rule1)) -> rule6) triple3) -> rule2)) -> rule8))] Anne is rough.[(triple3)] Anne is round.[(triple4)] Dave is blue.[(triple5 OR ((triple7) -> rule4) OR ((triple8) -> rule5) OR ((((triple9) -> rule8)) -> rule4))] Dave is cold.[(triple6 OR ((triple7 triple9) -> rule3) OR ((((triple9) -> rule8) triple9) -> rule3))] Dave is quiet.[(triple7 OR ((triple9) -> rule8))] Dave is round.[(triple8)] Dave is smart.[(triple9)] Fiona is cold.[(triple10)] Fiona is rough.[(triple11)] Harry is cold.[(triple12 OR ((triple13) -> rule6) OR ((((triple15) -> rule8) triple15) -> rule3))] Harry is green.[(triple13)] Harry is round.[(triple14)] Harry is smart.[(triple15)] @1: Anne is green.[(((triple4) -> rule1))] Dave is green.[(((triple6 triple7) -> rule7) OR ((triple6 ((triple9) -> rule8)) -> rule7) OR ((((triple7 triple9) -> rule3) triple7) -> rule7) OR ((((triple7 triple9) -> rule3) ((triple9) -> rule8)) -> rule7) OR ((((((triple9) -> rule8) triple9) -> rule3) triple7) -> rule7) OR ((((((triple9) -> rule8) triple9) -> rule3) ((triple9) -> rule8)) -> rule7))] Fiona is smart.[(((triple10 triple11) -> rule2))] Harry is blue.[(((triple14) -> rule5) OR ((((triple15) -> rule8)) -> rule4))] Harry is quiet.[(((triple15) -> rule8))] @2: Anne is cold.[(((((triple4) -> rule1)) -> rule6))] Fiona is quiet.[(((((triple10 triple11) -> rule2)) -> rule8))] @3: Anne is smart.[(((((((triple4) -> rule1)) -> rule6) triple3) -> rule2))] Fiona is blue.[(((((((triple10 triple11) -> rule2)) -> rule8)) -> rule4))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
((triple2) -> (rule4 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((triple4) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((((((((((triple4) -> (rule1 % int5))) -> (rule6 % int4)) triple3) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
int4
Anne is green.
("Anne" "is" "green" "+")
int5
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
((((((((triple4) -> (rule1 % int4))) -> (rule6 % int3)) triple3) -> (rule2 % int2))) -> (rule8 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
int4
Anne is rough.
("Anne" "is" "rough" "+")
triple3
Anne is round.
("Anne" "is" "round" "+")
triple4
Dave is blue.
("Dave" "is" "blue" "+")
triple5
((triple7) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((triple8) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((((triple9) -> (rule8 % int2))) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
triple6
((triple7 triple9) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((((triple9) -> (rule8 % int2)) triple9) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple7
((triple9) -> (rule8 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
triple8
Dave is smart.
("Dave" "is" "smart" "+")
triple9
Fiona is cold.
("Fiona" "is" "cold" "+")
triple10
Fiona is rough.
("Fiona" "is" "rough" "+")
triple11
Harry is cold.
("Harry" "is" "cold" "+")
triple12
((triple13) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((((triple15) -> (rule8 % int2)) triple15) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
triple13
Harry is round.
("Harry" "is" "round" "+")
triple14
Harry is smart.
("Harry" "is" "smart" "+")
triple15
Anne is green.
("Anne" "is" "green" "+")
((triple4) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((triple6 triple7) -> (rule7 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((triple6 ((triple9) -> (rule8 % int2))) -> (rule7 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
((((triple7 triple9) -> (rule3 % int2)) triple7) -> (rule7 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
((((triple7 triple9) -> (rule3 % int3)) ((triple9) -> (rule8 % int2))) -> (rule7 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
((((((triple9) -> (rule8 % int3)) triple9) -> (rule3 % int2)) triple7) -> (rule7 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
((((((triple9) -> (rule8 % int3)) triple9) -> (rule3 % int2)) ((triple9) -> (rule8 % int3))) -> (rule7 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple10 triple11) -> (rule2 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple14) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((((triple15) -> (rule8 % int2))) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple15) -> (rule8 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
((((triple4) -> (rule1 % int2))) -> (rule6 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((((triple10 triple11) -> (rule2 % int2))) -> (rule8 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
((((((triple4) -> (rule1 % int3))) -> (rule6 % int2)) triple3) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Fiona is blue.
("Fiona" "is" "blue" "+")
((((((triple10 triple11) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3