The cow chases the tiger. The cow is blue. The cow is cold. The cow is nice. The cow is round. The cow needs the tiger. The cow does not see the tiger. The tiger chases the cow. The tiger is blue. The tiger is cold. The tiger is nice. The tiger is not round. The tiger is young. The tiger does not need the cow. The tiger sees the cow. All cold, blue people are young.
The cow chases the tiger.
("cow" "chases" "tiger" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow is round.
("cow" "is" "round" "+")
The cow needs the tiger.
("cow" "needs" "tiger" "+")
The cow does not see the tiger.
("cow" "sees" "tiger" "-")
The tiger chases the cow.
("tiger" "chases" "cow" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is not round.
("tiger" "is" "round" "-")
The tiger is young.
("tiger" "is" "young" "+")
The tiger does not need the cow.
("tiger" "needs" "cow" "-")
The tiger sees the cow.
("tiger" "sees" "cow" "+")
All cold, blue people are young.
((("someone" "is" "cold" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
The tiger is nice.
True
1
proof
[(triple11)]
("tiger" "is" "nice" "+")
triple11
The tiger does not see the cow.
False
1
inv-proof
[(triple15)]
("tiger" "sees" "cow" "-")
triple15
The cow is young.
True
3
proof
[(((triple3 triple2) -> rule1))]
("cow" "is" "young" "+")
((triple3 triple2) -> (rule1 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is not young.
False
3
inv-proof
[(((triple3 triple2) -> rule1))]
("cow" "is" "young" "-")
((triple3 triple2) -> (rule1 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The tiger does not see the tiger.
Unknown
inv-random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "-")
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 need the cow.
Unknown
inv-random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "-")
The tiger chases the tiger.
Unknown
random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "+")
@0: The cow chases the tiger.[(triple1)] The cow does not see the tiger.[(triple7)] The cow is blue.[(triple2)] The cow is cold.[(triple3)] The cow is nice.[(triple4)] The cow is round.[(triple5)] The cow needs the tiger.[(triple6)] The tiger chases the cow.[(triple8)] The tiger does not need the cow.[(triple14)] The tiger is blue.[(triple9)] The tiger is cold.[(triple10)] The tiger is nice.[(triple11)] The tiger is not round.[(triple12)] The tiger is young.[(triple13 OR ((triple10 triple9) -> rule1))] The tiger sees the cow.[(triple15)] @1: The cow is young.[(((triple3 triple2) -> rule1))]
The cow chases the tiger.
("cow" "chases" "tiger" "+")
triple1
The cow does not see the tiger.
("cow" "sees" "tiger" "-")
triple7
The cow is blue.
("cow" "is" "blue" "+")
triple2
The cow is cold.
("cow" "is" "cold" "+")
triple3
The cow is nice.
("cow" "is" "nice" "+")
triple4
The cow is round.
("cow" "is" "round" "+")
triple5
The cow needs the tiger.
("cow" "needs" "tiger" "+")
triple6
The tiger chases the cow.
("tiger" "chases" "cow" "+")
triple8
The tiger does not need the cow.
("tiger" "needs" "cow" "-")
triple14
The tiger is blue.
("tiger" "is" "blue" "+")
triple9
The tiger is cold.
("tiger" "is" "cold" "+")
triple10
The tiger is nice.
("tiger" "is" "nice" "+")
triple11
The tiger is not round.
("tiger" "is" "round" "-")
triple12
The tiger is young.
("tiger" "is" "young" "+")
triple13
((triple10 triple9) -> (rule1 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger sees the cow.
("tiger" "sees" "cow" "+")
triple15
The cow is young.
("cow" "is" "young" "+")
((triple3 triple2) -> (rule1 % int1))
The cow is young.
("cow" "is" "young" "+")
int1