The cow visits the tiger. The tiger is nice. The tiger is red. The tiger is rough. The tiger likes the cow. The tiger needs the cow. The tiger visits the cow. If someone visits the cow then the cow visits the tiger. If someone is rough then they need the tiger. Cold people are round. If someone likes the cow then the cow likes the tiger. If the cow likes the tiger then the cow is cold. If someone is rough then they like the tiger.
The cow visits the tiger.
("cow" "visits" "tiger" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger likes the cow.
("tiger" "likes" "cow" "+")
The tiger needs the cow.
("tiger" "needs" "cow" "+")
The tiger visits the cow.
("tiger" "visits" "cow" "+")
If someone visits the cow then the cow visits the tiger.
((("someone" "visits" "cow" "+")) -> ("cow" "visits" "tiger" "+"))
If someone is rough then they need the tiger.
((("someone" "is" "rough" "+")) -> ("someone" "needs" "tiger" "+"))
Cold people are round.
((("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
If someone likes the cow then the cow likes the tiger.
((("someone" "likes" "cow" "+")) -> ("cow" "likes" "tiger" "+"))
If the cow likes the tiger then the cow is cold.
((("cow" "likes" "tiger" "+")) -> ("cow" "is" "cold" "+"))
If someone is rough then they like the tiger.
((("someone" "is" "rough" "+")) -> ("someone" "likes" "tiger" "+"))
The tiger is nice.
True
1
proof
[(triple2)]
("tiger" "is" "nice" "+")
triple2
The tiger is not rough.
False
1
inv-proof
[(triple4)]
("tiger" "is" "rough" "-")
triple4
The tiger likes the tiger.
True
2
proof
[(((triple4) -> rule6))]
("tiger" "likes" "tiger" "+")
((triple4) -> (rule6 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger does not like the tiger.
False
2
inv-proof
[(((triple4) -> rule6))]
("tiger" "likes" "tiger" "-")
((triple4) -> (rule6 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The cow is cold.
True
3
proof
[(((((triple5) -> rule4)) -> rule5))]
("cow" "is" "cold" "+")
((((triple5) -> (rule4 % int2))) -> (rule5 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int2
The cow is not cold.
False
3
inv-proof
[(((((triple5) -> rule4)) -> rule5))]
("cow" "is" "cold" "-")
((((triple5) -> (rule4 % int2))) -> (rule5 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int2
The cow is round.
True
4
proof
[(((((((triple5) -> rule4)) -> rule5)) -> rule3))]
("cow" "is" "round" "+")
((((((triple5) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int3
The cow is not round.
False
4
inv-proof
[(((((((triple5) -> rule4)) -> rule5)) -> rule3))]
("cow" "is" "round" "-")
((((((triple5) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int3
The tiger is not round.
Unknown
inv-rconc
[@1: The tiger is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "is" "round" "-")
The cow needs the tiger.
Unknown
rconc
[@1: The cow needs the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "needs" "tiger" "+")
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 cow.
Unknown
random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "+")
The tiger is not cold.
Unknown
inv-random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "-")
The cow is red.
Unknown
random
[@0: The cow is red.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "red" "+")
The cow does not like the cow.
Unknown
inv-random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cow" "-")
The cow needs the cow.
Unknown
random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "+")
@0: The cow visits the tiger.[(triple1 OR ((triple7) -> rule1))] The tiger is nice.[(triple2)] The tiger is red.[(triple3)] The tiger is rough.[(triple4)] The tiger likes the cow.[(triple5)] The tiger needs the cow.[(triple6)] The tiger visits the cow.[(triple7)] @1: The cow likes the tiger.[(((triple5) -> rule4))] The tiger likes the tiger.[(((triple4) -> rule6))] The tiger needs the tiger.[(((triple4) -> rule2))] @2: The cow is cold.[(((((triple5) -> rule4)) -> rule5))] @3: The cow is round.[(((((((triple5) -> rule4)) -> rule5)) -> rule3))]
The cow visits the tiger.
("cow" "visits" "tiger" "+")
triple1
((triple7) -> (rule1 % int1))
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
triple2
The tiger is red.
("tiger" "is" "red" "+")
triple3
The tiger is rough.
("tiger" "is" "rough" "+")
triple4
The tiger likes the cow.
("tiger" "likes" "cow" "+")
triple5
The tiger needs the cow.
("tiger" "needs" "cow" "+")
triple6
The tiger visits the cow.
("tiger" "visits" "cow" "+")
triple7
The cow likes the tiger.
("cow" "likes" "tiger" "+")
((triple5) -> (rule4 % int1))
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
((triple4) -> (rule6 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
((triple4) -> (rule2 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
((((triple5) -> (rule4 % int2))) -> (rule5 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int2
The cow is round.
("cow" "is" "round" "+")
((((((triple5) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int3