The cat eats the tiger. The cat is cold. The cat is young. The cat visits the tiger. The tiger is green. The tiger sees the cat. The tiger visits the cat. If something eats the cat and it eats the tiger then it sees the cat. If the cat eats the tiger then the cat sees the tiger. If something is young then it sees the tiger. If something eats the tiger then the tiger visits the cat. If something is young and it sees the tiger then the tiger is cold. If something eats the cat then it is green. If something is cold then it sees the cat. If something is young then it eats the tiger.
The cat eats the tiger.
("cat" "eats" "tiger" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat is young.
("cat" "is" "young" "+")
The cat visits the tiger.
("cat" "visits" "tiger" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger sees the cat.
("tiger" "sees" "cat" "+")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
If something eats the cat and it eats the tiger then it sees the cat.
((("something" "eats" "cat" "+") ("something" "eats" "tiger" "+")) -> ("something" "sees" "cat" "+"))
If the cat eats the tiger then the cat sees the tiger.
((("cat" "eats" "tiger" "+")) -> ("cat" "sees" "tiger" "+"))
If something is young then it sees the tiger.
((("something" "is" "young" "+")) -> ("something" "sees" "tiger" "+"))
If something eats the tiger then the tiger visits the cat.
((("something" "eats" "tiger" "+")) -> ("tiger" "visits" "cat" "+"))
If something is young and it sees the tiger then the tiger is cold.
((("something" "is" "young" "+") ("something" "sees" "tiger" "+")) -> ("tiger" "is" "cold" "+"))
If something eats the cat then it is green.
((("something" "eats" "cat" "+")) -> ("something" "is" "green" "+"))
If something is cold then it sees the cat.
((("something" "is" "cold" "+")) -> ("something" "sees" "cat" "+"))
If something is young then it eats the tiger.
((("something" "is" "young" "+")) -> ("something" "eats" "tiger" "+"))
The cat eats the tiger.
True
1
proof
[(triple1 OR ((triple3) -> rule8))]
("cat" "eats" "tiger" "+")
triple1
((triple3) -> (rule8 % int1))
The cat eats the tiger.
("cat" "eats" "tiger" "+")
int1
The tiger is not green.
False
1
inv-proof
[(triple5)]
("tiger" "is" "green" "-")
triple5
The cat sees the tiger.
True
2
proof
[(((triple1) -> rule2) OR ((triple3) -> rule3) OR ((((triple3) -> rule8)) -> rule2))]
("cat" "sees" "tiger" "+")
((triple1) -> (rule2 % int1))
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int1
((triple3) -> (rule3 % int1))
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int1
((((triple3) -> (rule8 % int2))) -> (rule2 % int1))
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int1
The cat eats the tiger.
("cat" "eats" "tiger" "+")
int2
The cat does not see the tiger.
False
2
inv-proof
[(((triple1) -> rule2) OR ((triple3) -> rule3) OR ((((triple3) -> rule8)) -> rule2))]
("cat" "sees" "tiger" "-")
((triple1) -> (rule2 % int1))
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int1
((triple3) -> (rule3 % int1))
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int1
((((triple3) -> (rule8 % int2))) -> (rule2 % int1))
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int1
The cat eats the tiger.
("cat" "eats" "tiger" "+")
int2
The tiger is cold.
True
4
proof
[(((triple3 ((triple1) -> rule2)) -> rule5) OR ((triple3 ((triple3) -> rule3)) -> rule5) OR ((triple3 ((((triple3) -> rule8)) -> rule2)) -> rule5))]
("tiger" "is" "cold" "+")
((triple3 ((triple1) -> (rule2 % int2))) -> (rule5 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int2
((triple3 ((triple3) -> (rule3 % int2))) -> (rule5 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int2
((triple3 ((((triple3) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int2
The cat eats the tiger.
("cat" "eats" "tiger" "+")
int3
The tiger is not cold.
False
4
inv-proof
[(((triple3 ((triple1) -> rule2)) -> rule5) OR ((triple3 ((triple3) -> rule3)) -> rule5) OR ((triple3 ((((triple3) -> rule8)) -> rule2)) -> rule5))]
("tiger" "is" "cold" "-")
((triple3 ((triple1) -> (rule2 % int2))) -> (rule5 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int2
((triple3 ((triple3) -> (rule3 % int2))) -> (rule5 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int2
((triple3 ((((triple3) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int2
The cat eats the tiger.
("cat" "eats" "tiger" "+")
int3
The tiger does not eat the tiger.
Unknown
inv-rconc
[@1: The tiger eats the tiger.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("tiger" "eats" "tiger" "-")
The tiger sees the tiger.
Unknown
rconc
[@1: The tiger sees the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "sees" "tiger" "+")
The cat is not green.
Unknown
inv-rconc
[@1: The cat is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "is" "green" "-")
The tiger eats the cat.
Unknown
random
[@0: The tiger eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "cat" "+")
The cat does not eat the cat.
Unknown
inv-random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "-")
The tiger is young.
Unknown
random
[@0: The tiger is young.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "young" "+")
@0: The cat eats the tiger.[(triple1 OR ((triple3) -> rule8))] The cat is cold.[(triple2)] The cat is young.[(triple3)] The cat visits the tiger.[(triple4)] The tiger is green.[(triple5)] The tiger sees the cat.[(triple6 OR ((((triple3 ((triple1) -> rule2)) -> rule5)) -> rule7) OR ((((triple3 ((triple3) -> rule3)) -> rule5)) -> rule7) OR ((((triple3 ((((triple3) -> rule8)) -> rule2)) -> rule5)) -> rule7))] The tiger visits the cat.[(triple7 OR ((triple1) -> rule4) OR ((((triple3) -> rule8)) -> rule4))] @1: The cat sees the cat.[(((triple2) -> rule7))] The cat sees the tiger.[(((triple1) -> rule2) OR ((triple3) -> rule3) OR ((((triple3) -> rule8)) -> rule2))] @2: The tiger is cold.[(((triple3 ((triple1) -> rule2)) -> rule5) OR ((triple3 ((triple3) -> rule3)) -> rule5) OR ((triple3 ((((triple3) -> rule8)) -> rule2)) -> rule5))]
The cat eats the tiger.
("cat" "eats" "tiger" "+")
triple1
((triple3) -> (rule8 % int1))
The cat eats the tiger.
("cat" "eats" "tiger" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
triple2
The cat is young.
("cat" "is" "young" "+")
triple3
The cat visits the tiger.
("cat" "visits" "tiger" "+")
triple4
The tiger is green.
("tiger" "is" "green" "+")
triple5
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple6
((((triple3 ((triple1) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int3
((((triple3 ((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int3
((((triple3 ((((triple3) -> (rule8 % int4))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int3
The cat eats the tiger.
("cat" "eats" "tiger" "+")
int4
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple7
((triple1) -> (rule4 % int1))
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int1
((((triple3) -> (rule8 % int2))) -> (rule4 % int1))
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int1
The cat eats the tiger.
("cat" "eats" "tiger" "+")
int2
The cat sees the cat.
("cat" "sees" "cat" "+")
((triple2) -> (rule7 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
((triple1) -> (rule2 % int1))
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int1
((triple3) -> (rule3 % int1))
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int1
((((triple3) -> (rule8 % int2))) -> (rule2 % int1))
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int1
The cat eats the tiger.
("cat" "eats" "tiger" "+")
int2
The tiger is cold.
("tiger" "is" "cold" "+")
((triple3 ((triple1) -> (rule2 % int2))) -> (rule5 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int2
((triple3 ((triple3) -> (rule3 % int2))) -> (rule5 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int2
((triple3 ((((triple3) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int2
The cat eats the tiger.
("cat" "eats" "tiger" "+")
int3