The cow eats the tiger. The cow is round. The cow visits the rabbit. The dog eats the rabbit. The dog visits the cow. The rabbit is kind. The tiger is not big. The tiger is cold. The tiger is round. The tiger sees the dog. The tiger visits the dog. If someone is cold then they see the dog. If someone eats the tiger then they eat the cow. If someone eats the dog then the dog is big. If the tiger is cold then the tiger does not visit the rabbit. If someone eats the dog then the dog is round. If someone sees the rabbit then the rabbit eats the tiger. If someone is kind then they visit the dog. If someone visits the cow and they see the rabbit then the cow does not visit the tiger. If someone eats the cow then they see the rabbit.
The cow eats the tiger.
("cow" "eats" "tiger" "+")
The cow is round.
("cow" "is" "round" "+")
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
The dog visits the cow.
("dog" "visits" "cow" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The tiger is not big.
("tiger" "is" "big" "-")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger sees the dog.
("tiger" "sees" "dog" "+")
The tiger visits the dog.
("tiger" "visits" "dog" "+")
If someone is cold then they see the dog.
((("someone" "is" "cold" "+")) -> ("someone" "sees" "dog" "+"))
If someone eats the tiger then they eat the cow.
((("someone" "eats" "tiger" "+")) -> ("someone" "eats" "cow" "+"))
If someone eats the dog then the dog is big.
((("someone" "eats" "dog" "+")) -> ("dog" "is" "big" "+"))
If the tiger is cold then the tiger does not visit the rabbit.
((("tiger" "is" "cold" "+")) -> ("tiger" "visits" "rabbit" "-"))
If someone eats the dog then the dog is round.
((("someone" "eats" "dog" "+")) -> ("dog" "is" "round" "+"))
If someone sees the rabbit then the rabbit eats the tiger.
((("someone" "sees" "rabbit" "+")) -> ("rabbit" "eats" "tiger" "+"))
If someone is kind then they visit the dog.
((("someone" "is" "kind" "+")) -> ("someone" "visits" "dog" "+"))
If someone visits the cow and they see the rabbit then the cow does not visit the tiger.
((("someone" "visits" "cow" "+") ("someone" "sees" "rabbit" "+")) -> ("cow" "visits" "tiger" "-"))
If someone eats the cow then they see the rabbit.
((("someone" "eats" "cow" "+")) -> ("someone" "sees" "rabbit" "+"))
The dog eats the rabbit.
True
1
proof
[(triple4)]
("dog" "eats" "rabbit" "+")
triple4
The cow does not eat the tiger.
False
1
inv-proof
[(triple1)]
("cow" "eats" "tiger" "-")
triple1
The rabbit visits the dog.
True
2
proof
[(((triple6) -> rule7))]
("rabbit" "visits" "dog" "+")
((triple6) -> (rule7 % int1))
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int1
The cow does not eat the cow.
False
2
inv-proof
[(((triple1) -> rule2))]
("cow" "eats" "cow" "-")
((triple1) -> (rule2 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow sees the rabbit.
True
3
proof
[(((((triple1) -> rule2)) -> rule9))]
("cow" "sees" "rabbit" "+")
((((triple1) -> (rule2 % int2))) -> (rule9 % int1))
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2
The cow does not see the rabbit.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule9))]
("cow" "sees" "rabbit" "-")
((((triple1) -> (rule2 % int2))) -> (rule9 % int1))
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2
The rabbit eats the tiger.
True
4
proof
[(((((((triple1) -> rule2)) -> rule9)) -> rule6))]
("rabbit" "eats" "tiger" "+")
((((((triple1) -> (rule2 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int1
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int2
The cow eats the cow.
("cow" "eats" "cow" "+")
int3
The rabbit does not eat the tiger.
False
4
inv-proof
[(((((((triple1) -> rule2)) -> rule9)) -> rule6))]
("rabbit" "eats" "tiger" "-")
((((((triple1) -> (rule2 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int1
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int2
The cow eats the cow.
("cow" "eats" "cow" "+")
int3
The rabbit eats the cow.
True
5
proof
[(((((((((triple1) -> rule2)) -> rule9)) -> rule6)) -> rule2))]
("rabbit" "eats" "cow" "+")
((((((((triple1) -> (rule2 % int4))) -> (rule9 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int1
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int2
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int3
The cow eats the cow.
("cow" "eats" "cow" "+")
int4
The rabbit does not eat the cow.
False
5
inv-proof
[(((((((((triple1) -> rule2)) -> rule9)) -> rule6)) -> rule2))]
("rabbit" "eats" "cow" "-")
((((((((triple1) -> (rule2 % int4))) -> (rule9 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int1
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int2
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int3
The cow eats the cow.
("cow" "eats" "cow" "+")
int4
The rabbit sees the rabbit.
True
6
proof
[(((((((((((triple1) -> rule2)) -> rule9)) -> rule6)) -> rule2)) -> rule9))]
("rabbit" "sees" "rabbit" "+")
((((((((((triple1) -> (rule2 % int5))) -> (rule9 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule9 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int2
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int3
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int4
The cow eats the cow.
("cow" "eats" "cow" "+")
int5
The rabbit does not see the rabbit.
False
6
inv-proof
[(((((((((((triple1) -> rule2)) -> rule9)) -> rule6)) -> rule2)) -> rule9))]
("rabbit" "sees" "rabbit" "-")
((((((((((triple1) -> (rule2 % int5))) -> (rule9 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule9 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int2
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int3
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int4
The cow eats the cow.
("cow" "eats" "cow" "+")
int5
The dog is not big.
Unknown
inv-rconc
[@1: The dog is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "is" "big" "-")
The dog visits the dog.
Unknown
rconc
[@1: The dog visits the dog.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("dog" "visits" "dog" "+")
The tiger does not eat the cow.
Unknown
inv-rconc
[@1: The tiger eats the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "eats" "cow" "-")
The dog eats the cow.
Unknown
rconc
[@1: The dog eats the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "eats" "cow" "+")
The dog is not round.
Unknown
inv-rconc
[@1: The dog is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "is" "round" "-")
The dog sees the dog.
Unknown
rconc
[@1: The dog sees the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "sees" "dog" "+")
The dog is not nice.
Unknown
inv-random
[@0: The dog is nice.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "nice" "-")
The cow is kind.
Unknown
random
[@0: The cow is kind.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "kind" "+")
The tiger does not eat the tiger.
Unknown
inv-random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "-")
The dog visits the tiger.
Unknown
random
[@0: The dog visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "tiger" "+")
The dog does not eat the tiger.
Unknown
inv-random
[@0: The dog eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "tiger" "-")
The dog is cold.
Unknown
random
[@0: The dog is cold.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "cold" "+")
@0: The cow eats the tiger.[(triple1)] The cow is round.[(triple2)] The cow visits the rabbit.[(triple3)] The dog eats the rabbit.[(triple4)] The dog visits the cow.[(triple5)] The rabbit is kind.[(triple6)] The tiger is cold.[(triple8)] The tiger is not big.[(triple7)] The tiger is round.[(triple9)] The tiger sees the dog.[(triple10 OR ((triple8) -> rule1))] The tiger visits the dog.[(triple11)] @1: The cow eats the cow.[(((triple1) -> rule2))] The rabbit visits the dog.[(((triple6) -> rule7))] The tiger does not visit the rabbit.[(((triple8) -> rule4))] @2: The cow sees the rabbit.[(((((triple1) -> rule2)) -> rule9))] @3: The rabbit eats the tiger.[(((((((triple1) -> rule2)) -> rule9)) -> rule6))] @4: The rabbit eats the cow.[(((((((((triple1) -> rule2)) -> rule9)) -> rule6)) -> rule2))] @5: The rabbit sees the rabbit.[(((((((((((triple1) -> rule2)) -> rule9)) -> rule6)) -> rule2)) -> rule9))]
The cow eats the tiger.
("cow" "eats" "tiger" "+")
triple1
The cow is round.
("cow" "is" "round" "+")
triple2
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
triple3
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
triple4
The dog visits the cow.
("dog" "visits" "cow" "+")
triple5
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple6
The tiger is cold.
("tiger" "is" "cold" "+")
triple8
The tiger is not big.
("tiger" "is" "big" "-")
triple7
The tiger is round.
("tiger" "is" "round" "+")
triple9
The tiger sees the dog.
("tiger" "sees" "dog" "+")
triple10
((triple8) -> (rule1 % int1))
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int1
The tiger visits the dog.
("tiger" "visits" "dog" "+")
triple11
The cow eats the cow.
("cow" "eats" "cow" "+")
((triple1) -> (rule2 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
((triple6) -> (rule7 % int1))
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int1
The tiger does not visit the rabbit.
("tiger" "visits" "rabbit" "-")
((triple8) -> (rule4 % int1))
The tiger does not visit the rabbit.
("tiger" "visits" "rabbit" "-")
int1
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
((((triple1) -> (rule2 % int2))) -> (rule9 % int1))
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
((((((triple1) -> (rule2 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int1
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int2
The cow eats the cow.
("cow" "eats" "cow" "+")
int3
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
((((((((triple1) -> (rule2 % int4))) -> (rule9 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int1
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int2
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int3
The cow eats the cow.
("cow" "eats" "cow" "+")
int4
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
((((((((((triple1) -> (rule2 % int5))) -> (rule9 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule9 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int2
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int3
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int4
The cow eats the cow.
("cow" "eats" "cow" "+")
int5