The bear is young. The bear likes the cat. The cat is young. If something eats the cat then the cat sees the bear. If the bear is young then the bear likes the cat. If something sees the bear then the bear eats the cat. If something is rough then it sees the bear. If something likes the cat then it sees the bear. If something eats the cat then the cat likes the bear.
The bear is young.
("bear" "is" "young" "+")
The bear likes the cat.
("bear" "likes" "cat" "+")
The cat is young.
("cat" "is" "young" "+")
If something eats the cat then the cat sees the bear.
((("something" "eats" "cat" "+")) -> ("cat" "sees" "bear" "+"))
If the bear is young then the bear likes the cat.
((("bear" "is" "young" "+")) -> ("bear" "likes" "cat" "+"))
If something sees the bear then the bear eats the cat.
((("something" "sees" "bear" "+")) -> ("bear" "eats" "cat" "+"))
If something is rough then it sees the bear.
((("something" "is" "rough" "+")) -> ("something" "sees" "bear" "+"))
If something likes the cat then it sees the bear.
((("something" "likes" "cat" "+")) -> ("something" "sees" "bear" "+"))
If something eats the cat then the cat likes the bear.
((("something" "eats" "cat" "+")) -> ("cat" "likes" "bear" "+"))
The bear is young.
True
1
proof
[(triple1)]
("bear" "is" "young" "+")
triple1
The cat is not young.
False
1
inv-proof
[(triple3)]
("cat" "is" "young" "-")
triple3
The bear sees the bear.
True
2
proof
[(((triple2) -> rule5) OR ((((triple1) -> rule2)) -> rule5))]
("bear" "sees" "bear" "+")
((triple2) -> (rule5 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The bear likes the cat.
("bear" "likes" "cat" "+")
int2
The bear does not see the bear.
False
2
inv-proof
[(((triple2) -> rule5) OR ((((triple1) -> rule2)) -> rule5))]
("bear" "sees" "bear" "-")
((triple2) -> (rule5 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The bear likes the cat.
("bear" "likes" "cat" "+")
int2
The bear eats the cat.
True
3
proof
[(((((triple2) -> rule5)) -> rule3) OR ((((((triple1) -> rule2)) -> rule5)) -> rule3))]
("bear" "eats" "cat" "+")
((((triple2) -> (rule5 % int2))) -> (rule3 % int1))
The bear eats the cat.
("bear" "eats" "cat" "+")
int1
The bear sees the bear.
("bear" "sees" "bear" "+")
int2
((((((triple1) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The bear eats the cat.
("bear" "eats" "cat" "+")
int1
The bear sees the bear.
("bear" "sees" "bear" "+")
int2
The bear likes the cat.
("bear" "likes" "cat" "+")
int3
The bear does not eat the cat.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule3) OR ((((((triple1) -> rule2)) -> rule5)) -> rule3))]
("bear" "eats" "cat" "-")
((((triple2) -> (rule5 % int2))) -> (rule3 % int1))
The bear eats the cat.
("bear" "eats" "cat" "+")
int1
The bear sees the bear.
("bear" "sees" "bear" "+")
int2
((((((triple1) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The bear eats the cat.
("bear" "eats" "cat" "+")
int1
The bear sees the bear.
("bear" "sees" "bear" "+")
int2
The bear likes the cat.
("bear" "likes" "cat" "+")
int3
The cat sees the bear.
True
4
proof
[(((((((triple2) -> rule5)) -> rule3)) -> rule1) OR ((((((((triple1) -> rule2)) -> rule5)) -> rule3)) -> rule1))]
("cat" "sees" "bear" "+")
((((((triple2) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The cat sees the bear.
("cat" "sees" "bear" "+")
int1
The bear eats the cat.
("bear" "eats" "cat" "+")
int2
The bear sees the bear.
("bear" "sees" "bear" "+")
int3
((((((((triple1) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The cat sees the bear.
("cat" "sees" "bear" "+")
int1
The bear eats the cat.
("bear" "eats" "cat" "+")
int2
The bear sees the bear.
("bear" "sees" "bear" "+")
int3
The bear likes the cat.
("bear" "likes" "cat" "+")
int4
The cat does not like the bear.
False
4
inv-proof
[(((((((triple2) -> rule5)) -> rule3)) -> rule6) OR ((((((((triple1) -> rule2)) -> rule5)) -> rule3)) -> rule6))]
("cat" "likes" "bear" "-")
((((((triple2) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The cat likes the bear.
("cat" "likes" "bear" "+")
int1
The bear eats the cat.
("bear" "eats" "cat" "+")
int2
The bear sees the bear.
("bear" "sees" "bear" "+")
int3
((((((((triple1) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The cat likes the bear.
("cat" "likes" "bear" "+")
int1
The bear eats the cat.
("bear" "eats" "cat" "+")
int2
The bear sees the bear.
("bear" "sees" "bear" "+")
int3
The bear likes the cat.
("bear" "likes" "cat" "+")
int4
The bear is not cold.
Unknown
inv-random
[@0: The bear is cold.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "cold" "-")
The cat eats the bear.
Unknown
random
[@0: The cat eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "bear" "+")
The bear is not nice.
Unknown
inv-random
[@0: The bear is nice.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "nice" "-")
The cat is nice.
Unknown
random
[@0: The cat is nice.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "nice" "+")
The bear is not rough.
Unknown
inv-random
[@0: The bear is rough.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "rough" "-")
The cat sees the cat.
Unknown
random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "+")
The cat is not rough.
Unknown
inv-random
[@0: The cat is rough.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "rough" "-")
The bear is red.
Unknown
random
[@0: The bear is red.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "red" "+")
@0: The bear is young.[(triple1)] The bear likes the cat.[(triple2 OR ((triple1) -> rule2))] The cat is young.[(triple3)] @1: The bear sees the bear.[(((triple2) -> rule5) OR ((((triple1) -> rule2)) -> rule5))] @2: The bear eats the cat.[(((((triple2) -> rule5)) -> rule3) OR ((((((triple1) -> rule2)) -> rule5)) -> rule3))] @3: The cat likes the bear.[(((((((triple2) -> rule5)) -> rule3)) -> rule6) OR ((((((((triple1) -> rule2)) -> rule5)) -> rule3)) -> rule6))] The cat sees the bear.[(((((((triple2) -> rule5)) -> rule3)) -> rule1) OR ((((((((triple1) -> rule2)) -> rule5)) -> rule3)) -> rule1))]
The bear is young.
("bear" "is" "young" "+")
triple1
The bear likes the cat.
("bear" "likes" "cat" "+")
triple2
((triple1) -> (rule2 % int1))
The bear likes the cat.
("bear" "likes" "cat" "+")
int1
The cat is young.
("cat" "is" "young" "+")
triple3
The bear sees the bear.
("bear" "sees" "bear" "+")
((triple2) -> (rule5 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The bear likes the cat.
("bear" "likes" "cat" "+")
int2
The bear eats the cat.
("bear" "eats" "cat" "+")
((((triple2) -> (rule5 % int2))) -> (rule3 % int1))
The bear eats the cat.
("bear" "eats" "cat" "+")
int1
The bear sees the bear.
("bear" "sees" "bear" "+")
int2
((((((triple1) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The bear eats the cat.
("bear" "eats" "cat" "+")
int1
The bear sees the bear.
("bear" "sees" "bear" "+")
int2
The bear likes the cat.
("bear" "likes" "cat" "+")
int3
The cat likes the bear.
("cat" "likes" "bear" "+")
((((((triple2) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The cat likes the bear.
("cat" "likes" "bear" "+")
int1
The bear eats the cat.
("bear" "eats" "cat" "+")
int2
The bear sees the bear.
("bear" "sees" "bear" "+")
int3
((((((((triple1) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The cat likes the bear.
("cat" "likes" "bear" "+")
int1
The bear eats the cat.
("bear" "eats" "cat" "+")
int2
The bear sees the bear.
("bear" "sees" "bear" "+")
int3
The bear likes the cat.
("bear" "likes" "cat" "+")
int4
The cat sees the bear.
("cat" "sees" "bear" "+")
((((((triple2) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The cat sees the bear.
("cat" "sees" "bear" "+")
int1
The bear eats the cat.
("bear" "eats" "cat" "+")
int2
The bear sees the bear.
("bear" "sees" "bear" "+")
int3
((((((((triple1) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The cat sees the bear.
("cat" "sees" "bear" "+")
int1
The bear eats the cat.
("bear" "eats" "cat" "+")
int2
The bear sees the bear.
("bear" "sees" "bear" "+")
int3
The bear likes the cat.
("bear" "likes" "cat" "+")
int4