The cat chases the cow. The cat visits the cow. The cat visits the squirrel. The cow chases the tiger. The cow is kind. The cow visits the squirrel. The cow visits the tiger. The squirrel chases the cow. The squirrel visits the tiger. The tiger is big. If something chases the cow and it sees the cat then it is big. If something is nice and it sees the tiger then it visits the squirrel. If something visits the cow and the cow sees the cat then the cow is big. If something chases the tiger then it chases the squirrel. If something is green then it chases the cow. If something is kind and it visits the cat then it sees the squirrel. If something is big then it chases the tiger. If something chases the squirrel then it sees the cow.
The cat chases the cow.
("cat" "chases" "cow" "+")
The cat visits the cow.
("cat" "visits" "cow" "+")
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
The cow chases the tiger.
("cow" "chases" "tiger" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
The cow visits the tiger.
("cow" "visits" "tiger" "+")
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
The tiger is big.
("tiger" "is" "big" "+")
If something chases the cow and it sees the cat then it is big.
((("something" "chases" "cow" "+") ("something" "sees" "cat" "+")) -> ("something" "is" "big" "+"))
If something is nice and it sees the tiger then it visits the squirrel.
((("something" "is" "nice" "+") ("something" "sees" "tiger" "+")) -> ("something" "visits" "squirrel" "+"))
If something visits the cow and the cow sees the cat then the cow is big.
((("something" "visits" "cow" "+") ("cow" "sees" "cat" "+")) -> ("cow" "is" "big" "+"))
If something chases the tiger then it chases the squirrel.
((("something" "chases" "tiger" "+")) -> ("something" "chases" "squirrel" "+"))
If something is green then it chases the cow.
((("something" "is" "green" "+")) -> ("something" "chases" "cow" "+"))
If something is kind and it visits the cat then it sees the squirrel.
((("something" "is" "kind" "+") ("something" "visits" "cat" "+")) -> ("something" "sees" "squirrel" "+"))
If something is big then it chases the tiger.
((("something" "is" "big" "+")) -> ("something" "chases" "tiger" "+"))
If something chases the squirrel then it sees the cow.
((("something" "chases" "squirrel" "+")) -> ("something" "sees" "cow" "+"))
The squirrel visits the tiger.
True
1
proof
[(triple9)]
("squirrel" "visits" "tiger" "+")
triple9
The squirrel does not chase the cow.
False
1
inv-proof
[(triple8)]
("squirrel" "chases" "cow" "-")
triple8
The tiger chases the tiger.
True
2
proof
[(((triple10) -> rule7))]
("tiger" "chases" "tiger" "+")
((triple10) -> (rule7 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The cow does not chase the squirrel.
False
2
inv-proof
[(((triple4) -> rule4))]
("cow" "chases" "squirrel" "-")
((triple4) -> (rule4 % int1))
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
int1
The cow sees the cow.
True
3
proof
[(((((triple4) -> rule4)) -> rule8))]
("cow" "sees" "cow" "+")
((((triple4) -> (rule4 % int2))) -> (rule8 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
int2
The tiger does not chase the squirrel.
False
3
inv-proof
[(((((triple10) -> rule7)) -> rule4))]
("tiger" "chases" "squirrel" "-")
((((triple10) -> (rule7 % int2))) -> (rule4 % int1))
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int2
The tiger sees the cow.
True
4
proof
[(((((((triple10) -> rule7)) -> rule4)) -> rule8))]
("tiger" "sees" "cow" "+")
((((((triple10) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int1
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int2
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int3
The tiger does not see the cow.
False
4
inv-proof
[(((((((triple10) -> rule7)) -> rule4)) -> rule8))]
("tiger" "sees" "cow" "-")
((((((triple10) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int1
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int2
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int3
The cow does not chase the cow.
Unknown
inv-rconc
[@1: The cow chases the cow.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "chases" "cow" "-")
The cat sees the cow.
Unknown
rconc
[@4: The cat sees the cow.[CWA. Example of deepest failure = (rule8 <- rule4 <- rule7 <- rule1 <- FAIL)]]
("cat" "sees" "cow" "+")
The squirrel does not visit the squirrel.
Unknown
inv-rconc
[@1: The squirrel visits the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "visits" "squirrel" "-")
The cat sees the squirrel.
Unknown
rconc
[@1: The cat sees the squirrel.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "sees" "squirrel" "+")
The tiger does not see the tiger.
Unknown
inv-random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "-")
The cow is green.
Unknown
random
[@0: The cow is green.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "green" "+")
The cow does not see the tiger.
Unknown
inv-random
[@0: The cow sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "tiger" "-")
The cow is nice.
Unknown
random
[@0: The cow is nice.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "nice" "+")
@0: The cat chases the cow.[(triple1)] The cat visits the cow.[(triple2)] The cat visits the squirrel.[(triple3)] The cow chases the tiger.[(triple4)] The cow is kind.[(triple5)] The cow visits the squirrel.[(triple6)] The cow visits the tiger.[(triple7)] The squirrel chases the cow.[(triple8)] The squirrel visits the tiger.[(triple9)] The tiger is big.[(triple10)] @1: The cow chases the squirrel.[(((triple4) -> rule4))] The tiger chases the tiger.[(((triple10) -> rule7))] @2: The cow sees the cow.[(((((triple4) -> rule4)) -> rule8))] The tiger chases the squirrel.[(((((triple10) -> rule7)) -> rule4))] @3: The tiger sees the cow.[(((((((triple10) -> rule7)) -> rule4)) -> rule8))]
The cat chases the cow.
("cat" "chases" "cow" "+")
triple1
The cat visits the cow.
("cat" "visits" "cow" "+")
triple2
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
triple3
The cow chases the tiger.
("cow" "chases" "tiger" "+")
triple4
The cow is kind.
("cow" "is" "kind" "+")
triple5
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
triple6
The cow visits the tiger.
("cow" "visits" "tiger" "+")
triple7
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
triple8
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
triple9
The tiger is big.
("tiger" "is" "big" "+")
triple10
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
((triple4) -> (rule4 % int1))
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
((triple10) -> (rule7 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The cow sees the cow.
("cow" "sees" "cow" "+")
((((triple4) -> (rule4 % int2))) -> (rule8 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
int2
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
((((triple10) -> (rule7 % int2))) -> (rule4 % int1))
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int2
The tiger sees the cow.
("tiger" "sees" "cow" "+")
((((((triple10) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int1
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int2
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int3