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