The bear chases the lion. The cat is nice. The cow is rough. The lion sees the bear. If something is nice then it chases the cow. If the cat is nice and the cat is green then the cat sees the bear. If something chases the cow then the cow sees the cat. If something is big and it chases the bear then it chases the cow. If something sees the cat then it visits the bear. If something chases the cat and the cat sees the cow then the cow is red.
The bear chases the lion.
("bear" "chases" "lion" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cow is rough.
("cow" "is" "rough" "+")
The lion sees the bear.
("lion" "sees" "bear" "+")
If something is nice then it chases the cow.
((("something" "is" "nice" "+")) -> ("something" "chases" "cow" "+"))
If the cat is nice and the cat is green then the cat sees the bear.
((("cat" "is" "nice" "+") ("cat" "is" "green" "+")) -> ("cat" "sees" "bear" "+"))
If something chases the cow then the cow sees the cat.
((("something" "chases" "cow" "+")) -> ("cow" "sees" "cat" "+"))
If something is big and it chases the bear then it chases the cow.
((("something" "is" "big" "+") ("something" "chases" "bear" "+")) -> ("something" "chases" "cow" "+"))
If something sees the cat then it visits the bear.
((("something" "sees" "cat" "+")) -> ("something" "visits" "bear" "+"))
If something chases the cat and the cat sees the cow then the cow is red.
((("something" "chases" "cat" "+") ("cat" "sees" "cow" "+")) -> ("cow" "is" "red" "+"))
The lion sees the bear.
True
1
proof
[(triple4)]
("lion" "sees" "bear" "+")
triple4
The lion does not see the bear.
False
1
inv-proof
[(triple4)]
("lion" "sees" "bear" "-")
triple4
The cat chases the cow.
True
2
proof
[(((triple2) -> rule1))]
("cat" "chases" "cow" "+")
((triple2) -> (rule1 % int1))
The cat chases the cow.
("cat" "chases" "cow" "+")
int1
The cat does not chase the cow.
False
2
inv-proof
[(((triple2) -> rule1))]
("cat" "chases" "cow" "-")
((triple2) -> (rule1 % int1))
The cat chases the cow.
("cat" "chases" "cow" "+")
int1
The cow sees the cat.
True
3
proof
[(((((triple2) -> rule1)) -> rule3))]
("cow" "sees" "cat" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The cow sees the cat.
("cow" "sees" "cat" "+")
int1
The cat chases the cow.
("cat" "chases" "cow" "+")
int2
The cow does not see the cat.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule3))]
("cow" "sees" "cat" "-")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The cow sees the cat.
("cow" "sees" "cat" "+")
int1
The cat chases the cow.
("cat" "chases" "cow" "+")
int2
The cow visits the bear.
True
4
proof
[(((((((triple2) -> rule1)) -> rule3)) -> rule5))]
("cow" "visits" "bear" "+")
((((((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The cow visits the bear.
("cow" "visits" "bear" "+")
int1
The cow sees the cat.
("cow" "sees" "cat" "+")
int2
The cat chases the cow.
("cat" "chases" "cow" "+")
int3
The cow does not visit the bear.
False
4
inv-proof
[(((((((triple2) -> rule1)) -> rule3)) -> rule5))]
("cow" "visits" "bear" "-")
((((((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The cow visits the bear.
("cow" "visits" "bear" "+")
int1
The cow sees the cat.
("cow" "sees" "cat" "+")
int2
The cat chases the cow.
("cat" "chases" "cow" "+")
int3
The cow does not chase the cow.
Unknown
inv-rconc
[@1: The cow chases the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "chases" "cow" "-")
The cow is red.
Unknown
rconc
[@1: The cow is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "is" "red" "+")
The lion does not chase the cow.
Unknown
inv-rconc
[@1: The lion chases the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "chases" "cow" "-")
The lion visits the bear.
Unknown
rconc
[@1: The lion visits the bear.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "visits" "bear" "+")
The cat is not red.
Unknown
inv-random
[@0: The cat is red.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "red" "-")
The cat chases the bear.
Unknown
random
[@0: The cat chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "bear" "+")
The cow is not nice.
Unknown
inv-random
[@0: The cow is nice.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "nice" "-")
The cow sees the lion.
Unknown
random
[@0: The cow sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "lion" "+")
@0: The bear chases the lion.[(triple1)] The cat is nice.[(triple2)] The cow is rough.[(triple3)] The lion sees the bear.[(triple4)] @1: The cat chases the cow.[(((triple2) -> rule1))] @2: The cow sees the cat.[(((((triple2) -> rule1)) -> rule3))] @3: The cow visits the bear.[(((((((triple2) -> rule1)) -> rule3)) -> rule5))]
The bear chases the lion.
("bear" "chases" "lion" "+")
triple1
The cat is nice.
("cat" "is" "nice" "+")
triple2
The cow is rough.
("cow" "is" "rough" "+")
triple3
The lion sees the bear.
("lion" "sees" "bear" "+")
triple4
The cat chases the cow.
("cat" "chases" "cow" "+")
((triple2) -> (rule1 % int1))
The cat chases the cow.
("cat" "chases" "cow" "+")
int1
The cow sees the cat.
("cow" "sees" "cat" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The cow sees the cat.
("cow" "sees" "cat" "+")
int1
The cat chases the cow.
("cat" "chases" "cow" "+")
int2
The cow visits the bear.
("cow" "visits" "bear" "+")
((((((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The cow visits the bear.
("cow" "visits" "bear" "+")
int1
The cow sees the cat.
("cow" "sees" "cat" "+")
int2
The cat chases the cow.
("cat" "chases" "cow" "+")
int3