The bear is blue. The bear is cold. The bear is red. The bear is rough. The bear is round. The bear likes the cat. The bear sees the cat. The bear visits the cat. The cat is blue. The cat is cold. The cat is red. The cat is rough. The cat likes the bear. The cat sees the bear. The cat visits the bear. If someone is rough then they see the cat. If someone sees the cat then they visit the cat.
The bear is blue.
("bear" "is" "blue" "+")
The bear is cold.
("bear" "is" "cold" "+")
The bear is red.
("bear" "is" "red" "+")
The bear is rough.
("bear" "is" "rough" "+")
The bear is round.
("bear" "is" "round" "+")
The bear likes the cat.
("bear" "likes" "cat" "+")
The bear sees the cat.
("bear" "sees" "cat" "+")
The bear visits the cat.
("bear" "visits" "cat" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat is red.
("cat" "is" "red" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat likes the bear.
("cat" "likes" "bear" "+")
The cat sees the bear.
("cat" "sees" "bear" "+")
The cat visits the bear.
("cat" "visits" "bear" "+")
If someone is rough then they see the cat.
((("someone" "is" "rough" "+")) -> ("someone" "sees" "cat" "+"))
If someone sees the cat then they visit the cat.
((("someone" "sees" "cat" "+")) -> ("someone" "visits" "cat" "+"))
The bear is red.
True
1
proof
[(triple3)]
("bear" "is" "red" "+")
triple3
The bear is not cold.
False
1
inv-proof
[(triple2)]
("bear" "is" "cold" "-")
triple2
The cat sees the cat.
True
2
proof
[(((triple12) -> rule1))]
("cat" "sees" "cat" "+")
((triple12) -> (rule1 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat does not see the cat.
False
2
inv-proof
[(((triple12) -> rule1))]
("cat" "sees" "cat" "-")
((triple12) -> (rule1 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat visits the cat.
True
3
proof
[(((((triple12) -> rule1)) -> rule2))]
("cat" "visits" "cat" "+")
((((triple12) -> (rule1 % int2))) -> (rule2 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2
The cat does not visit the cat.
False
3
inv-proof
[(((((triple12) -> rule1)) -> rule2))]
("cat" "visits" "cat" "-")
((((triple12) -> (rule1 % int2))) -> (rule2 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2
The cat is not round.
Unknown
inv-random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "-")
The bear sees the bear.
Unknown
random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "+")
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 bear likes the bear.
Unknown
random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "+")
@0: The bear is blue.[(triple1)] The bear is cold.[(triple2)] The bear is red.[(triple3)] The bear is rough.[(triple4)] The bear is round.[(triple5)] The bear likes the cat.[(triple6)] The bear sees the cat.[(triple7 OR ((triple4) -> rule1))] The bear visits the cat.[(triple8 OR ((triple7) -> rule2) OR ((((triple4) -> rule1)) -> rule2))] The cat is blue.[(triple9)] The cat is cold.[(triple10)] The cat is red.[(triple11)] The cat is rough.[(triple12)] The cat likes the bear.[(triple13)] The cat sees the bear.[(triple14)] The cat visits the bear.[(triple15)] @1: The cat sees the cat.[(((triple12) -> rule1))] @2: The cat visits the cat.[(((((triple12) -> rule1)) -> rule2))]
The bear is blue.
("bear" "is" "blue" "+")
triple1
The bear is cold.
("bear" "is" "cold" "+")
triple2
The bear is red.
("bear" "is" "red" "+")
triple3
The bear is rough.
("bear" "is" "rough" "+")
triple4
The bear is round.
("bear" "is" "round" "+")
triple5
The bear likes the cat.
("bear" "likes" "cat" "+")
triple6
The bear sees the cat.
("bear" "sees" "cat" "+")
triple7
((triple4) -> (rule1 % int1))
The bear sees the cat.
("bear" "sees" "cat" "+")
int1
The bear visits the cat.
("bear" "visits" "cat" "+")
triple8
((triple7) -> (rule2 % int1))
The bear visits the cat.
("bear" "visits" "cat" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
The bear visits the cat.
("bear" "visits" "cat" "+")
int1
The bear sees the cat.
("bear" "sees" "cat" "+")
int2
The cat is blue.
("cat" "is" "blue" "+")
triple9
The cat is cold.
("cat" "is" "cold" "+")
triple10
The cat is red.
("cat" "is" "red" "+")
triple11
The cat is rough.
("cat" "is" "rough" "+")
triple12
The cat likes the bear.
("cat" "likes" "bear" "+")
triple13
The cat sees the bear.
("cat" "sees" "bear" "+")
triple14
The cat visits the bear.
("cat" "visits" "bear" "+")
triple15
The cat sees the cat.
("cat" "sees" "cat" "+")
((triple12) -> (rule1 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
((((triple12) -> (rule1 % int2))) -> (rule2 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2