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