The cat is big. The cat is cold. The cat is kind. The cat is nice. The cat is red. If someone is kind and cold then they are big. All big people are kind. All red people are kind. If the cat is red and the cat is big then the cat is nice. All big people are nice. All nice, red people are kind. If the cat is nice and the cat is big then the cat is cold. All nice people are cold.
The cat is big.
("cat" "is" "big" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat is red.
("cat" "is" "red" "+")
If someone is kind and cold then they are big.
((("someone" "is" "kind" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
All big people are kind.
((("someone" "is" "big" "+")) -> ("someone" "is" "kind" "+"))
All red people are kind.
((("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
If the cat is red and the cat is big then the cat is nice.
((("cat" "is" "red" "+") ("cat" "is" "big" "+")) -> ("cat" "is" "nice" "+"))
All big people are nice.
((("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
All nice, red people are kind.
((("someone" "is" "nice" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
If the cat is nice and the cat is big then the cat is cold.
((("cat" "is" "nice" "+") ("cat" "is" "big" "+")) -> ("cat" "is" "cold" "+"))
All nice people are cold.
((("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
The cat is red.
True
1
proof
[(triple5)]
("cat" "is" "red" "+")
triple5
The cat is not big.
False
1
inv-proof
[(triple1 OR ((triple3 triple2) -> rule1) OR ((triple3 ((triple4) -> rule8)) -> rule1) OR ((((triple5) -> rule3) triple2) -> rule1) OR ((((triple4 triple5) -> rule6) triple2) -> rule1) OR ((((triple5) -> rule3) ((triple4) -> rule8)) -> rule1) OR ((((triple4 triple5) -> rule6) ((triple4) -> rule8)) -> rule1))]
("cat" "is" "big" "-")
triple1
((triple3 triple2) -> (rule1 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
((triple3 ((triple4) -> (rule8 % int2))) -> (rule1 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
((((triple5) -> (rule3 % int2)) triple2) -> (rule1 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
((((triple4 triple5) -> (rule6 % int2)) triple2) -> (rule1 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
((((triple5) -> (rule3 % int3)) ((triple4) -> (rule8 % int2))) -> (rule1 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The cat is kind.
("cat" "is" "kind" "+")
int3
((((triple4 triple5) -> (rule6 % int3)) ((triple4) -> (rule8 % int2))) -> (rule1 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The cat is kind.
("cat" "is" "kind" "+")
int3
The cat does not like the cat.
Unknown
inv-random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "-")
The cat sees the cat.
Unknown
random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "+")
@0: The cat is big.[(triple1 OR ((triple3 triple2) -> rule1) OR ((triple3 ((triple4) -> rule8)) -> rule1) OR ((((triple5) -> rule3) triple2) -> rule1) OR ((((triple4 triple5) -> rule6) triple2) -> rule1) OR ((((triple5) -> rule3) ((triple4) -> rule8)) -> rule1) OR ((((triple4 triple5) -> rule6) ((triple4) -> rule8)) -> rule1))] The cat is cold.[(triple2 OR ((triple4) -> rule8) OR ((triple4 triple1) -> rule7) OR ((((triple1) -> rule5)) -> rule8) OR ((((triple5 triple1) -> rule4)) -> rule8) OR ((((triple1) -> rule5) triple1) -> rule7) OR ((((triple5 triple1) -> rule4) triple1) -> rule7))] The cat is kind.[(triple3 OR ((triple1) -> rule2) OR ((triple5) -> rule3) OR ((triple4 triple5) -> rule6) OR ((((triple1) -> rule5) triple5) -> rule6) OR ((((triple5 triple1) -> rule4) triple5) -> rule6))] The cat is nice.[(triple4 OR ((triple1) -> rule5) OR ((triple5 triple1) -> rule4) OR ((((triple3 triple2) -> rule1)) -> rule5) OR ((triple5 ((triple3 triple2) -> rule1)) -> rule4) OR ((((((triple5) -> rule3) triple2) -> rule1)) -> rule5) OR ((triple5 ((((triple5) -> rule3) triple2) -> rule1)) -> rule4))] The cat is red.[(triple5)]
The cat is big.
("cat" "is" "big" "+")
triple1
((triple3 triple2) -> (rule1 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
((triple3 ((triple4) -> (rule8 % int2))) -> (rule1 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
((((triple5) -> (rule3 % int2)) triple2) -> (rule1 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
((((triple4 triple5) -> (rule6 % int2)) triple2) -> (rule1 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
((((triple5) -> (rule3 % int3)) ((triple4) -> (rule8 % int2))) -> (rule1 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The cat is kind.
("cat" "is" "kind" "+")
int3
((((triple4 triple5) -> (rule6 % int3)) ((triple4) -> (rule8 % int2))) -> (rule1 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The cat is kind.
("cat" "is" "kind" "+")
int3
The cat is cold.
("cat" "is" "cold" "+")
triple2
((triple4) -> (rule8 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
((triple4 triple1) -> (rule7 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
((((triple1) -> (rule5 % int2))) -> (rule8 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
((((triple5 triple1) -> (rule4 % int2))) -> (rule8 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
((((triple1) -> (rule5 % int2)) triple1) -> (rule7 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
((((triple5 triple1) -> (rule4 % int2)) triple1) -> (rule7 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat is kind.
("cat" "is" "kind" "+")
triple3
((triple1) -> (rule2 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
((triple5) -> (rule3 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
((triple4 triple5) -> (rule6 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
((((triple1) -> (rule5 % int2)) triple5) -> (rule6 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
((((triple5 triple1) -> (rule4 % int2)) triple5) -> (rule6 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat is nice.
("cat" "is" "nice" "+")
triple4
((triple1) -> (rule5 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
((triple5 triple1) -> (rule4 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
((((triple3 triple2) -> (rule1 % int2))) -> (rule5 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
((triple5 ((triple3 triple2) -> (rule1 % int2))) -> (rule4 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
((((((triple5) -> (rule3 % int3)) triple2) -> (rule1 % int2))) -> (rule5 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The cat is kind.
("cat" "is" "kind" "+")
int3
((triple5 ((((triple5) -> (rule3 % int3)) triple2) -> (rule1 % int2))) -> (rule4 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The cat is kind.
("cat" "is" "kind" "+")
int3
The cat is red.
("cat" "is" "red" "+")
triple5