The cat eats the cow. The cat is not green. The cat is not rough. The cat does not visit the cow. The cat visits the squirrel. The cow is green. The squirrel eats the cow. The squirrel eats the tiger. The squirrel visits the cat. The tiger eats the squirrel. The tiger sees the squirrel. The tiger visits the cow. Rough things are red. If something visits the cat then it is rough. If something visits the squirrel and it eats the cow then it is cold. If something is cold then it visits the tiger. If something is red and it eats the cow then it visits the squirrel. If something eats the cat and it is not rough then it does not eat the cow. If something eats the cow and the cow does not see the cat then the cat is round. If something eats the cat and the cat visits the squirrel then the cat sees the squirrel. If something is red and it visits the tiger then the tiger sees the cat.
The cat eats the cow.
("cat" "eats" "cow" "+")
The cat is not green.
("cat" "is" "green" "-")
The cat is not rough.
("cat" "is" "rough" "-")
The cat does not visit the cow.
("cat" "visits" "cow" "-")
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
The cow is green.
("cow" "is" "green" "+")
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
The tiger visits the cow.
("tiger" "visits" "cow" "+")
Rough things are red.
((("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
If something visits the cat then it is rough.
((("something" "visits" "cat" "+")) -> ("something" "is" "rough" "+"))
If something visits the squirrel and it eats the cow then it is cold.
((("something" "visits" "squirrel" "+") ("something" "eats" "cow" "+")) -> ("something" "is" "cold" "+"))
If something is cold then it visits the tiger.
((("something" "is" "cold" "+")) -> ("something" "visits" "tiger" "+"))
If something is red and it eats the cow then it visits the squirrel.
((("something" "is" "red" "+") ("something" "eats" "cow" "+")) -> ("something" "visits" "squirrel" "+"))
If something eats the cat and it is not rough then it does not eat the cow.
((("something" "eats" "cat" "+") ("something" "is" "rough" "~")) -> ("something" "eats" "cow" "-"))
If something eats the cow and the cow does not see the cat then the cat is round.
((("something" "eats" "cow" "+") ("cow" "sees" "cat" "~")) -> ("cat" "is" "round" "+"))
If something eats the cat and the cat visits the squirrel then the cat sees the squirrel.
((("something" "eats" "cat" "+") ("cat" "visits" "squirrel" "+")) -> ("cat" "sees" "squirrel" "+"))
If something is red and it visits the tiger then the tiger sees the cat.
((("something" "is" "red" "+") ("something" "visits" "tiger" "+")) -> ("tiger" "sees" "cat" "+"))
The cat visits the squirrel.
True
1
proof
[(triple5)]
("cat" "visits" "squirrel" "+")
triple5
The tiger does not visit the cow.
False
1
inv-proof
[(triple12)]
("tiger" "visits" "cow" "-")
triple12
The cat is cold.
True
3
proof
[(((triple5 triple1) -> rule3))]
("cat" "is" "cold" "+")
((triple5 triple1) -> (rule3 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The squirrel is not rough.
False
2
inv-proof
[(((triple9) -> rule2))]
("squirrel" "is" "rough" "-")
((triple9) -> (rule2 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel is red.
True
3
proof
[(((((triple9) -> rule2)) -> rule1))]
("squirrel" "is" "red" "+")
((((triple9) -> (rule2 % int2))) -> (rule1 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The cat does not visit the tiger.
False
4
inv-proof
[(((((triple5 triple1) -> rule3)) -> rule4))]
("cat" "visits" "tiger" "-")
((((triple5 triple1) -> (rule3 % int2))) -> (rule4 % int1))
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The squirrel visits the squirrel.
True
5
proof
[(((((((triple9) -> rule2)) -> rule1) triple7) -> rule5))]
("squirrel" "visits" "squirrel" "+")
((((((triple9) -> (rule2 % int3))) -> (rule1 % int2)) triple7) -> (rule5 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The squirrel is rough.
("squirrel" "is" "rough" "+")
int3
The squirrel does not visit the squirrel.
False
5
inv-proof
[(((((((triple9) -> rule2)) -> rule1) triple7) -> rule5))]
("squirrel" "visits" "squirrel" "-")
((((((triple9) -> (rule2 % int3))) -> (rule1 % int2)) triple7) -> (rule5 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The squirrel is rough.
("squirrel" "is" "rough" "+")
int3
The squirrel is cold.
True
7
proof
[(((((((((triple9) -> rule2)) -> rule1) triple7) -> rule5) triple7) -> rule3))]
("squirrel" "is" "cold" "+")
((((((((triple9) -> (rule2 % int4))) -> (rule1 % int3)) triple7) -> (rule5 % int2)) triple7) -> (rule3 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int2
The squirrel is red.
("squirrel" "is" "red" "+")
int3
The squirrel is rough.
("squirrel" "is" "rough" "+")
int4
The squirrel is not cold.
False
7
inv-proof
[(((((((((triple9) -> rule2)) -> rule1) triple7) -> rule5) triple7) -> rule3))]
("squirrel" "is" "cold" "-")
((((((((triple9) -> (rule2 % int4))) -> (rule1 % int3)) triple7) -> (rule5 % int2)) triple7) -> (rule3 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int2
The squirrel is red.
("squirrel" "is" "red" "+")
int3
The squirrel is rough.
("squirrel" "is" "rough" "+")
int4
The squirrel visits the tiger.
True
8
proof
[(((((((((((triple9) -> rule2)) -> rule1) triple7) -> rule5) triple7) -> rule3)) -> rule4))]
("squirrel" "visits" "tiger" "+")
((((((((((triple9) -> (rule2 % int5))) -> (rule1 % int4)) triple7) -> (rule5 % int3)) triple7) -> (rule3 % int2))) -> (rule4 % int1))
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int3
The squirrel is red.
("squirrel" "is" "red" "+")
int4
The squirrel is rough.
("squirrel" "is" "rough" "+")
int5
The squirrel does not visit the tiger.
False
8
inv-proof
[(((((((((((triple9) -> rule2)) -> rule1) triple7) -> rule5) triple7) -> rule3)) -> rule4))]
("squirrel" "visits" "tiger" "-")
((((((((((triple9) -> (rule2 % int5))) -> (rule1 % int4)) triple7) -> (rule5 % int3)) triple7) -> (rule3 % int2))) -> (rule4 % int1))
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int3
The squirrel is red.
("squirrel" "is" "red" "+")
int4
The squirrel is rough.
("squirrel" "is" "rough" "+")
int5
The cow is not red.
Unknown
inv-rconc
[@2: The cow is red.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("cow" "is" "red" "-")
The tiger is cold.
Unknown
rconc
[@1: The tiger is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "is" "cold" "+")
The cat does not see the squirrel.
Unknown
inv-rconc
[@1: The cat sees the squirrel.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cat" "sees" "squirrel" "-")
The tiger visits the squirrel.
Unknown
rconc
[@1: The tiger visits the squirrel.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "visits" "squirrel" "+")
The cat is not round.
Unknown
inv-rconc
[@1: The cat is round.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cat" "is" "round" "-")
The cat is red.
Unknown
rconc
[@1: The cat is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "is" "red" "+")
The squirrel does not see the tiger.
Unknown
inv-random
[@0: The squirrel sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "tiger" "-")
The squirrel is green.
Unknown
random
[@0: The squirrel is green.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "green" "+")
The cow does not see the cow.
Unknown
inv-random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "-")
The cow sees the tiger.
Unknown
random
[@0: The cow sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "tiger" "+")
The cow does not eat the cat.
Unknown
inv-random
[@0: The cow eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cat" "-")
The squirrel sees the cat.
Unknown
random
[@0: The squirrel sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "cat" "+")
@0: The cat does not visit the cow.[(triple4)] The cat eats the cow.[(triple1)] The cat is not green.[(triple2)] The cat is not rough.[(triple3)] The cat visits the squirrel.[(triple5)] The cow is green.[(triple6)] The squirrel eats the cow.[(triple7)] The squirrel eats the tiger.[(triple8)] The squirrel visits the cat.[(triple9)] The tiger eats the squirrel.[(triple10)] The tiger sees the squirrel.[(triple11)] The tiger visits the cow.[(triple12)] @1: The cat is cold.[(((triple5 triple1) -> rule3))] The squirrel is rough.[(((triple9) -> rule2))] @2: The cat visits the tiger.[(((((triple5 triple1) -> rule3)) -> rule4))] The squirrel is red.[(((((triple9) -> rule2)) -> rule1))] @3: The squirrel visits the squirrel.[(((((((triple9) -> rule2)) -> rule1) triple7) -> rule5))] @4: The squirrel is cold.[(((((((((triple9) -> rule2)) -> rule1) triple7) -> rule5) triple7) -> rule3))] @5: The squirrel visits the tiger.[(((((((((((triple9) -> rule2)) -> rule1) triple7) -> rule5) triple7) -> rule3)) -> rule4))] @6: The tiger sees the cat.[(((((((triple9) -> rule2)) -> rule1) ((((((((((triple9) -> rule2)) -> rule1) triple7) -> rule5) triple7) -> rule3)) -> rule4)) -> rule9))]
The cat does not visit the cow.
("cat" "visits" "cow" "-")
triple4
The cat eats the cow.
("cat" "eats" "cow" "+")
triple1
The cat is not green.
("cat" "is" "green" "-")
triple2
The cat is not rough.
("cat" "is" "rough" "-")
triple3
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
triple5
The cow is green.
("cow" "is" "green" "+")
triple6
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
triple7
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
triple8
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
triple9
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
triple10
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
triple11
The tiger visits the cow.
("tiger" "visits" "cow" "+")
triple12
The cat is cold.
("cat" "is" "cold" "+")
((triple5 triple1) -> (rule3 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
((triple9) -> (rule2 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The cat visits the tiger.
("cat" "visits" "tiger" "+")
((((triple5 triple1) -> (rule3 % int2))) -> (rule4 % int1))
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The squirrel is red.
("squirrel" "is" "red" "+")
((((triple9) -> (rule2 % int2))) -> (rule1 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
((((((triple9) -> (rule2 % int3))) -> (rule1 % int2)) triple7) -> (rule5 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The squirrel is rough.
("squirrel" "is" "rough" "+")
int3
The squirrel is cold.
("squirrel" "is" "cold" "+")
((((((((triple9) -> (rule2 % int4))) -> (rule1 % int3)) triple7) -> (rule5 % int2)) triple7) -> (rule3 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int2
The squirrel is red.
("squirrel" "is" "red" "+")
int3
The squirrel is rough.
("squirrel" "is" "rough" "+")
int4
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
((((((((((triple9) -> (rule2 % int5))) -> (rule1 % int4)) triple7) -> (rule5 % int3)) triple7) -> (rule3 % int2))) -> (rule4 % int1))
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int3
The squirrel is red.
("squirrel" "is" "red" "+")
int4
The squirrel is rough.
("squirrel" "is" "rough" "+")
int5
The tiger sees the cat.
("tiger" "sees" "cat" "+")
((((((triple9) -> (rule2 % int6))) -> (rule1 % int5)) ((((((((((triple9) -> (rule2 % int6))) -> (rule1 % int5)) triple7) -> (rule5 % int4)) triple7) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule9 % int1))
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int1
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
int3
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int4
The squirrel is red.
("squirrel" "is" "red" "+")
int5
The squirrel is rough.
("squirrel" "is" "rough" "+")
int6