The cow is blue. The cow is red. The cow sees the rabbit. The cow sees the tiger. The rabbit chases the cow. The rabbit chases the tiger. The rabbit is nice. The rabbit is red. The rabbit is rough. The tiger chases the cow. The tiger needs the cow. The tiger sees the rabbit. If something chases the cow and it sees the rabbit then it needs the rabbit. If something is big and it chases the cow then the cow is rough. If the tiger chases the cow and the cow is rough then the cow sees the rabbit. If something needs the rabbit then it does not chase the tiger. If the cow is big then the cow is blue. If something needs the tiger then it chases the cow. If something sees the tiger and it does not need the cow then the cow sees the tiger. If something sees the rabbit then it needs the tiger.
The cow is blue.
("cow" "is" "blue" "+")
The cow is red.
("cow" "is" "red" "+")
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
The cow sees the tiger.
("cow" "sees" "tiger" "+")
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The tiger chases the cow.
("tiger" "chases" "cow" "+")
The tiger needs the cow.
("tiger" "needs" "cow" "+")
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
If something chases the cow and it sees the rabbit then it needs the rabbit.
((("something" "chases" "cow" "+") ("something" "sees" "rabbit" "+")) -> ("something" "needs" "rabbit" "+"))
If something is big and it chases the cow then the cow is rough.
((("something" "is" "big" "+") ("something" "chases" "cow" "+")) -> ("cow" "is" "rough" "+"))
If the tiger chases the cow and the cow is rough then the cow sees the rabbit.
((("tiger" "chases" "cow" "+") ("cow" "is" "rough" "+")) -> ("cow" "sees" "rabbit" "+"))
If something needs the rabbit then it does not chase the tiger.
((("something" "needs" "rabbit" "+")) -> ("something" "chases" "tiger" "-"))
If the cow is big then the cow is blue.
((("cow" "is" "big" "+")) -> ("cow" "is" "blue" "+"))
If something needs the tiger then it chases the cow.
((("something" "needs" "tiger" "+")) -> ("something" "chases" "cow" "+"))
If something sees the tiger and it does not need the cow then the cow sees the tiger.
((("something" "sees" "tiger" "+") ("something" "needs" "cow" "~")) -> ("cow" "sees" "tiger" "+"))
If something sees the rabbit then it needs the tiger.
((("something" "sees" "rabbit" "+")) -> ("something" "needs" "tiger" "+"))
The tiger chases the cow.
True
1
proof
[(triple10 OR ((((triple12) -> rule8)) -> rule6))]
("tiger" "chases" "cow" "+")
triple10
((((triple12) -> (rule8 % int2))) -> (rule6 % int1))
The tiger chases the cow.
("tiger" "chases" "cow" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int2
The cow does not see the tiger.
False
1
inv-proof
[(triple4)]
("cow" "sees" "tiger" "-")
triple4
The cow needs the tiger.
True
2
proof
[(((triple3) -> rule8))]
("cow" "needs" "tiger" "+")
((triple3) -> (rule8 % int1))
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int1
The tiger does not need the rabbit.
False
3
inv-proof
[(((triple10 triple12) -> rule1) OR ((((((triple12) -> rule8)) -> rule6) triple12) -> rule1))]
("tiger" "needs" "rabbit" "-")
((triple10 triple12) -> (rule1 % int1))
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
int1
((((((triple12) -> (rule8 % int3))) -> (rule6 % int2)) triple12) -> (rule1 % int1))
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
int1
The tiger chases the cow.
("tiger" "chases" "cow" "+")
int2
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int3
The tiger does not chase the tiger.
True
4
proof
[(((((triple10 triple12) -> rule1)) -> rule4) OR ((((((((triple12) -> rule8)) -> rule6) triple12) -> rule1)) -> rule4))]
("tiger" "chases" "tiger" "-")
((((triple10 triple12) -> (rule1 % int2))) -> (rule4 % int1))
The tiger does not chase the tiger.
("tiger" "chases" "tiger" "-")
int1
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
int2
((((((((triple12) -> (rule8 % int4))) -> (rule6 % int3)) triple12) -> (rule1 % int2))) -> (rule4 % int1))
The tiger does not chase the tiger.
("tiger" "chases" "tiger" "-")
int1
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
int2
The tiger chases the cow.
("tiger" "chases" "cow" "+")
int3
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int4
The cow does not chase the cow.
False
3
inv-proof
[(((((triple3) -> rule8)) -> rule6))]
("cow" "chases" "cow" "-")
((((triple3) -> (rule8 % int2))) -> (rule6 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int2
The cow needs the rabbit.
True
5
proof
[(((((((triple3) -> rule8)) -> rule6) triple3) -> rule1))]
("cow" "needs" "rabbit" "+")
((((((triple3) -> (rule8 % int3))) -> (rule6 % int2)) triple3) -> (rule1 % int1))
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int3
The cow does not need the rabbit.
False
5
inv-proof
[(((((((triple3) -> rule8)) -> rule6) triple3) -> rule1))]
("cow" "needs" "rabbit" "-")
((((((triple3) -> (rule8 % int3))) -> (rule6 % int2)) triple3) -> (rule1 % int1))
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int3
The rabbit does not need the rabbit.
Unknown
inv-rconc
[@1: The rabbit needs the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "needs" "rabbit" "-")
The rabbit needs the tiger.
Unknown
rconc
[@1: The rabbit needs the tiger.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("rabbit" "needs" "tiger" "+")
The cow is not rough.
Unknown
inv-rconc
[@1: The cow is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "is" "rough" "-")
The rabbit sees the tiger.
Unknown
random
[@0: The rabbit sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "tiger" "+")
The cow does not need the cow.
Unknown
inv-random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "-")
The cow sees the cow.
Unknown
random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "+")
The cow does not chase the rabbit.
Unknown
inv-random
[@0: The cow chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "rabbit" "-")
The tiger is nice.
Unknown
random
[@0: The tiger is nice.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "nice" "+")
@0: The cow is blue.[(triple1)] The cow is red.[(triple2)] The cow sees the rabbit.[(triple3)] The cow sees the tiger.[(triple4)] The rabbit chases the cow.[(triple5)] The rabbit chases the tiger.[(triple6)] The rabbit is nice.[(triple7)] The rabbit is red.[(triple8)] The rabbit is rough.[(triple9)] The tiger chases the cow.[(triple10 OR ((((triple12) -> rule8)) -> rule6))] The tiger needs the cow.[(triple11)] The tiger sees the rabbit.[(triple12)] @1: The cow needs the tiger.[(((triple3) -> rule8))] The tiger needs the rabbit.[(((triple10 triple12) -> rule1) OR ((((((triple12) -> rule8)) -> rule6) triple12) -> rule1))] The tiger needs the tiger.[(((triple12) -> rule8))] @2: The cow chases the cow.[(((((triple3) -> rule8)) -> rule6))] The tiger does not chase the tiger.[(((((triple10 triple12) -> rule1)) -> rule4) OR ((((((((triple12) -> rule8)) -> rule6) triple12) -> rule1)) -> rule4))] @3: The cow needs the rabbit.[(((((((triple3) -> rule8)) -> rule6) triple3) -> rule1))] @4: The cow does not chase the tiger.[(((((((((triple3) -> rule8)) -> rule6) triple3) -> rule1)) -> rule4))]
The cow is blue.
("cow" "is" "blue" "+")
triple1
The cow is red.
("cow" "is" "red" "+")
triple2
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
triple3
The cow sees the tiger.
("cow" "sees" "tiger" "+")
triple4
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
triple5
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
triple6
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple7
The rabbit is red.
("rabbit" "is" "red" "+")
triple8
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple9
The tiger chases the cow.
("tiger" "chases" "cow" "+")
triple10
((((triple12) -> (rule8 % int2))) -> (rule6 % int1))
The tiger chases the cow.
("tiger" "chases" "cow" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int2
The tiger needs the cow.
("tiger" "needs" "cow" "+")
triple11
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
triple12
The cow needs the tiger.
("cow" "needs" "tiger" "+")
((triple3) -> (rule8 % int1))
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int1
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
((triple10 triple12) -> (rule1 % int1))
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
int1
((((((triple12) -> (rule8 % int3))) -> (rule6 % int2)) triple12) -> (rule1 % int1))
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
int1
The tiger chases the cow.
("tiger" "chases" "cow" "+")
int2
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int3
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
((triple12) -> (rule8 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
((((triple3) -> (rule8 % int2))) -> (rule6 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int2
The tiger does not chase the tiger.
("tiger" "chases" "tiger" "-")
((((triple10 triple12) -> (rule1 % int2))) -> (rule4 % int1))
The tiger does not chase the tiger.
("tiger" "chases" "tiger" "-")
int1
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
int2
((((((((triple12) -> (rule8 % int4))) -> (rule6 % int3)) triple12) -> (rule1 % int2))) -> (rule4 % int1))
The tiger does not chase the tiger.
("tiger" "chases" "tiger" "-")
int1
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
int2
The tiger chases the cow.
("tiger" "chases" "cow" "+")
int3
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int4
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
((((((triple3) -> (rule8 % int3))) -> (rule6 % int2)) triple3) -> (rule1 % int1))
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int3
The cow does not chase the tiger.
("cow" "chases" "tiger" "-")
((((((((triple3) -> (rule8 % int4))) -> (rule6 % int3)) triple3) -> (rule1 % int2))) -> (rule4 % int1))
The cow does not chase the tiger.
("cow" "chases" "tiger" "-")
int1
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int2
The cow chases the cow.
("cow" "chases" "cow" "+")
int3
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int4