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