The cow is big. The cow is cold. The cow is young. The cow likes the dog. The cow does not like the tiger. The cow visits the tiger. The dog chases the cow. The dog does not chase the tiger. The dog visits the cow. The tiger chases the cow. The tiger is big. The tiger is cold. The tiger likes the cow. The tiger visits the cow. The tiger does not visit the dog. If something chases the tiger then the tiger is cold. If something likes the tiger then it is round. If something is big then it is round. If something is cold then it visits the tiger. If something likes the cow and it is rough then it is young. If the dog is not cold then the dog chases the cow. If something likes the tiger and the tiger is not big then it visits the cow. If something is round then it chases the tiger.
The cow is big.
("cow" "is" "big" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow is young.
("cow" "is" "young" "+")
The cow likes the dog.
("cow" "likes" "dog" "+")
The cow does not like the tiger.
("cow" "likes" "tiger" "-")
The cow visits the tiger.
("cow" "visits" "tiger" "+")
The dog chases the cow.
("dog" "chases" "cow" "+")
The dog does not chase the tiger.
("dog" "chases" "tiger" "-")
The dog visits the cow.
("dog" "visits" "cow" "+")
The tiger chases the cow.
("tiger" "chases" "cow" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger likes the cow.
("tiger" "likes" "cow" "+")
The tiger visits the cow.
("tiger" "visits" "cow" "+")
The tiger does not visit the dog.
("tiger" "visits" "dog" "-")
If something chases the tiger then the tiger is cold.
((("something" "chases" "tiger" "+")) -> ("tiger" "is" "cold" "+"))
If something likes the tiger then it is round.
((("something" "likes" "tiger" "+")) -> ("something" "is" "round" "+"))
If something is big then it is round.
((("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
If something is cold then it visits the tiger.
((("something" "is" "cold" "+")) -> ("something" "visits" "tiger" "+"))
If something likes the cow and it is rough then it is young.
((("something" "likes" "cow" "+") ("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
If the dog is not cold then the dog chases the cow.
((("dog" "is" "cold" "~")) -> ("dog" "chases" "cow" "+"))
If something likes the tiger and the tiger is not big then it visits the cow.
((("something" "likes" "tiger" "+") ("tiger" "is" "big" "~")) -> ("something" "visits" "cow" "+"))
If something is round then it chases the tiger.
((("something" "is" "round" "+")) -> ("something" "chases" "tiger" "+"))
The dog chases the cow.
True
1
proof
[(triple7)]
("dog" "chases" "cow" "+")
triple7
The tiger is not big.
False
1
inv-proof
[(triple11)]
("tiger" "is" "big" "-")
triple11
The tiger is round.
True
2
proof
[(((triple11) -> rule3))]
("tiger" "is" "round" "+")
((triple11) -> (rule3 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger does not visit the tiger.
False
2
inv-proof
[(((triple12) -> rule4) OR ((((((((triple1) -> rule3)) -> rule8)) -> rule1)) -> rule4) OR ((((((((triple11) -> rule3)) -> rule8)) -> rule1)) -> rule4))]
("tiger" "visits" "tiger" "-")
((triple12) -> (rule4 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
((((((((triple1) -> (rule3 % int4))) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int3
The cow is round.
("cow" "is" "round" "+")
int4
((((((((triple11) -> (rule3 % int4))) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int3
The tiger is round.
("tiger" "is" "round" "+")
int4
The tiger chases the tiger.
True
3
proof
[(((((triple11) -> rule3)) -> rule8))]
("tiger" "chases" "tiger" "+")
((((triple11) -> (rule3 % int2))) -> (rule8 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
The tiger does not chase the tiger.
False
3
inv-proof
[(((((triple11) -> rule3)) -> rule8))]
("tiger" "chases" "tiger" "-")
((((triple11) -> (rule3 % int2))) -> (rule8 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
The cow does not visit the cow.
Unknown
inv-rconc
[@1: The cow visits the cow.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cow" "visits" "cow" "-")
The tiger is young.
Unknown
rconc
[@1: The tiger is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "is" "young" "+")
The dog is not round.
Unknown
inv-rconc
[@1: The dog is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "is" "round" "-")
The dog likes the cow.
Unknown
random
[@0: The dog likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "cow" "+")
The tiger is not rough.
Unknown
inv-random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "-")
The dog is rough.
Unknown
random
[@0: The dog is rough.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "rough" "+")
@0: The cow does not like the tiger.[(triple5)] The cow is big.[(triple1)] The cow is cold.[(triple2)] The cow is young.[(triple3)] The cow likes the dog.[(triple4)] The cow visits the tiger.[(triple6 OR ((triple2) -> rule4))] The dog chases the cow.[(triple7)] The dog does not chase the tiger.[(triple8)] The dog visits the cow.[(triple9)] The tiger chases the cow.[(triple10)] The tiger does not visit the dog.[(triple15)] The tiger is big.[(triple11)] The tiger is cold.[(triple12 OR ((((((triple1) -> rule3)) -> rule8)) -> rule1) OR ((((((triple11) -> rule3)) -> rule8)) -> rule1))] The tiger likes the cow.[(triple13)] The tiger visits the cow.[(triple14)] @1: The cow is round.[(((triple1) -> rule3))] The tiger is round.[(((triple11) -> rule3))] The tiger visits the tiger.[(((triple12) -> rule4) OR ((((((((triple1) -> rule3)) -> rule8)) -> rule1)) -> rule4) OR ((((((((triple11) -> rule3)) -> rule8)) -> rule1)) -> rule4))] @2: The cow chases the tiger.[(((((triple1) -> rule3)) -> rule8))] The tiger chases the tiger.[(((((triple11) -> rule3)) -> rule8))]
The cow does not like the tiger.
("cow" "likes" "tiger" "-")
triple5
The cow is big.
("cow" "is" "big" "+")
triple1
The cow is cold.
("cow" "is" "cold" "+")
triple2
The cow is young.
("cow" "is" "young" "+")
triple3
The cow likes the dog.
("cow" "likes" "dog" "+")
triple4
The cow visits the tiger.
("cow" "visits" "tiger" "+")
triple6
((triple2) -> (rule4 % int1))
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int1
The dog chases the cow.
("dog" "chases" "cow" "+")
triple7
The dog does not chase the tiger.
("dog" "chases" "tiger" "-")
triple8
The dog visits the cow.
("dog" "visits" "cow" "+")
triple9
The tiger chases the cow.
("tiger" "chases" "cow" "+")
triple10
The tiger does not visit the dog.
("tiger" "visits" "dog" "-")
triple15
The tiger is big.
("tiger" "is" "big" "+")
triple11
The tiger is cold.
("tiger" "is" "cold" "+")
triple12
((((((triple1) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int2
The cow is round.
("cow" "is" "round" "+")
int3
((((((triple11) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int2
The tiger is round.
("tiger" "is" "round" "+")
int3
The tiger likes the cow.
("tiger" "likes" "cow" "+")
triple13
The tiger visits the cow.
("tiger" "visits" "cow" "+")
triple14
The cow is round.
("cow" "is" "round" "+")
((triple1) -> (rule3 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
((triple11) -> (rule3 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
((triple12) -> (rule4 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
((((((((triple1) -> (rule3 % int4))) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int3
The cow is round.
("cow" "is" "round" "+")
int4
((((((((triple11) -> (rule3 % int4))) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int3
The tiger is round.
("tiger" "is" "round" "+")
int4
The cow chases the tiger.
("cow" "chases" "tiger" "+")
((((triple1) -> (rule3 % int2))) -> (rule8 % int1))
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int1
The cow is round.
("cow" "is" "round" "+")
int2
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
((((triple11) -> (rule3 % int2))) -> (rule8 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2