The cat eats the tiger. The cat is big. The cat is cold. The cat is kind. The cat is nice. The cat is round. The cat sees the tiger. The cat visits the tiger. The tiger eats the cat. The tiger is big. The tiger is cold. The tiger is kind. The tiger is nice. The tiger is round. The tiger sees the cat. The tiger visits the cat. If someone is cold then they are big. If someone visits the cat then the cat visits the tiger. If someone visits the cat then the cat visits the tiger.
The cat eats the tiger.
("cat" "eats" "tiger" "+")
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 round.
("cat" "is" "round" "+")
The cat sees the tiger.
("cat" "sees" "tiger" "+")
The cat visits the tiger.
("cat" "visits" "tiger" "+")
The tiger eats the cat.
("tiger" "eats" "cat" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger sees the cat.
("tiger" "sees" "cat" "+")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
If someone is cold then they are big.
((("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
If someone visits the cat then the cat visits the tiger.
((("someone" "visits" "cat" "+")) -> ("cat" "visits" "tiger" "+"))
If someone visits the cat then the cat visits the tiger.
((("someone" "visits" "cat" "+")) -> ("cat" "visits" "tiger" "+"))
The tiger eats the cat.
True
1
proof
[(triple9)]
("tiger" "eats" "cat" "+")
triple9
The cat is not kind.
False
1
inv-proof
[(triple4)]
("cat" "is" "kind" "-")
triple4
The tiger does not eat the tiger.
Unknown
inv-random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
@0: The cat eats the tiger.[(triple1)] The cat is big.[(triple2 OR ((triple3) -> rule1))] The cat is cold.[(triple3)] The cat is kind.[(triple4)] The cat is nice.[(triple5)] The cat is round.[(triple6)] The cat sees the tiger.[(triple7)] The cat visits the tiger.[(triple8 OR ((triple16) -> rule2) OR ((triple16) -> rule3))] The tiger eats the cat.[(triple9)] The tiger is big.[(triple10 OR ((triple11) -> rule1))] The tiger is cold.[(triple11)] The tiger is kind.[(triple12)] The tiger is nice.[(triple13)] The tiger is round.[(triple14)] The tiger sees the cat.[(triple15)] The tiger visits the cat.[(triple16)]
The cat eats the tiger.
("cat" "eats" "tiger" "+")
triple1
The cat is big.
("cat" "is" "big" "+")
triple2
((triple3) -> (rule1 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
triple3
The cat is kind.
("cat" "is" "kind" "+")
triple4
The cat is nice.
("cat" "is" "nice" "+")
triple5
The cat is round.
("cat" "is" "round" "+")
triple6
The cat sees the tiger.
("cat" "sees" "tiger" "+")
triple7
The cat visits the tiger.
("cat" "visits" "tiger" "+")
triple8
((triple16) -> (rule2 % int1))
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int1
((triple16) -> (rule3 % int1))
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int1
The tiger eats the cat.
("tiger" "eats" "cat" "+")
triple9
The tiger is big.
("tiger" "is" "big" "+")
triple10
((triple11) -> (rule1 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
triple11
The tiger is kind.
("tiger" "is" "kind" "+")
triple12
The tiger is nice.
("tiger" "is" "nice" "+")
triple13
The tiger is round.
("tiger" "is" "round" "+")
triple14
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple15
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple16