The cow likes the tiger. The tiger chases the cow. If something sees the cow then the cow is young. If something likes the tiger then it chases the cow. If something chases the cow then the cow likes the tiger. If something chases the cow then the cow is rough. If something likes the tiger and the tiger chases the cow then the cow chases the tiger. If something chases the tiger and it is red then the tiger is blue. If something sees the cow then the cow chases the tiger. If something chases the tiger then it likes the cow.
The cow likes the tiger.
("cow" "likes" "tiger" "+")
The tiger chases the cow.
("tiger" "chases" "cow" "+")
If something sees the cow then the cow is young.
((("something" "sees" "cow" "+")) -> ("cow" "is" "young" "+"))
If something likes the tiger then it chases the cow.
((("something" "likes" "tiger" "+")) -> ("something" "chases" "cow" "+"))
If something chases the cow then the cow likes the tiger.
((("something" "chases" "cow" "+")) -> ("cow" "likes" "tiger" "+"))
If something chases the cow then the cow is rough.
((("something" "chases" "cow" "+")) -> ("cow" "is" "rough" "+"))
If something likes the tiger and the tiger chases the cow then the cow chases the tiger.
((("something" "likes" "tiger" "+") ("tiger" "chases" "cow" "+")) -> ("cow" "chases" "tiger" "+"))
If something chases the tiger and it is red then the tiger is blue.
((("something" "chases" "tiger" "+") ("something" "is" "red" "+")) -> ("tiger" "is" "blue" "+"))
If something sees the cow then the cow chases the tiger.
((("something" "sees" "cow" "+")) -> ("cow" "chases" "tiger" "+"))
If something chases the tiger then it likes the cow.
((("something" "chases" "tiger" "+")) -> ("something" "likes" "cow" "+"))
The tiger chases the cow.
True
1
proof
[(triple2)]
("tiger" "chases" "cow" "+")
triple2
The cow does not like the tiger.
False
1
inv-proof
[(triple1 OR ((triple2) -> rule3))]
("cow" "likes" "tiger" "-")
triple1
((triple2) -> (rule3 % int1))
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int1
The cow is rough.
True
2
proof
[(((triple2) -> rule4) OR ((((triple1) -> rule2)) -> rule4) OR ((((((triple2) -> rule3)) -> rule2)) -> rule4))]
("cow" "is" "rough" "+")
((triple2) -> (rule4 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2
((((((triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int3
The cow does not chase the tiger.
False
3
inv-proof
[(((triple1 triple2) -> rule5) OR ((((triple2) -> rule3) triple2) -> rule5))]
("cow" "chases" "tiger" "-")
((triple1 triple2) -> (rule5 % int1))
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int1
((((triple2) -> (rule3 % int2)) triple2) -> (rule5 % int1))
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int1
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int2
The cow is not young.
Unknown
inv-rconc
[@1: The cow is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "is" "young" "-")
The tiger likes the cow.
Unknown
rconc
[@1: The tiger likes the cow.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("tiger" "likes" "cow" "+")
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 tiger is young.
Unknown
random
[@0: The tiger is young.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "young" "+")
@0: The cow likes the tiger.[(triple1 OR ((triple2) -> rule3))] The tiger chases the cow.[(triple2)] @1: The cow chases the cow.[(((triple1) -> rule2) OR ((((triple2) -> rule3)) -> rule2))] The cow chases the tiger.[(((triple1 triple2) -> rule5) OR ((((triple2) -> rule3) triple2) -> rule5))] The cow is rough.[(((triple2) -> rule4) OR ((((triple1) -> rule2)) -> rule4) OR ((((((triple2) -> rule3)) -> rule2)) -> rule4))] @2: The cow likes the cow.[(((((triple1 triple2) -> rule5)) -> rule8) OR ((((((triple2) -> rule3) triple2) -> rule5)) -> rule8))]
The cow likes the tiger.
("cow" "likes" "tiger" "+")
triple1
((triple2) -> (rule3 % int1))
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int1
The tiger chases the cow.
("tiger" "chases" "cow" "+")
triple2
The cow chases the cow.
("cow" "chases" "cow" "+")
((triple1) -> (rule2 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int2
The cow chases the tiger.
("cow" "chases" "tiger" "+")
((triple1 triple2) -> (rule5 % int1))
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int1
((((triple2) -> (rule3 % int2)) triple2) -> (rule5 % int1))
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int1
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int2
The cow is rough.
("cow" "is" "rough" "+")
((triple2) -> (rule4 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2
((((((triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int3
The cow likes the cow.
("cow" "likes" "cow" "+")
((((triple1 triple2) -> (rule5 % int2))) -> (rule8 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int2
((((((triple2) -> (rule3 % int3)) triple2) -> (rule5 % int2))) -> (rule8 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int2
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int3