The cow is cold. The cow likes the tiger. The cow needs the dog. The cow sees the dog. The dog likes the tiger. The lion is blue. The lion is green. The lion likes the dog. The lion likes the tiger. The lion sees the cow. The tiger likes the dog. The tiger needs the dog. The tiger sees the dog. The tiger sees the lion. If something sees the cow then it is kind. If something is blue and it likes the cow then it is cold. If something is green then it needs the lion. If something sees the tiger and the tiger is cold then the tiger sees the cow. If something likes the lion then it is kind. If something is kind and it sees the dog then it likes the cow. If something likes the cow then it is blue. If something needs the dog and the dog sees the cow then the dog is young. If something needs the dog then it likes the lion.
The cow is cold.
("cow" "is" "cold" "+")
The cow likes the tiger.
("cow" "likes" "tiger" "+")
The cow needs the dog.
("cow" "needs" "dog" "+")
The cow sees the dog.
("cow" "sees" "dog" "+")
The dog likes the tiger.
("dog" "likes" "tiger" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is green.
("lion" "is" "green" "+")
The lion likes the dog.
("lion" "likes" "dog" "+")
The lion likes the tiger.
("lion" "likes" "tiger" "+")
The lion sees the cow.
("lion" "sees" "cow" "+")
The tiger likes the dog.
("tiger" "likes" "dog" "+")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
The tiger sees the dog.
("tiger" "sees" "dog" "+")
The tiger sees the lion.
("tiger" "sees" "lion" "+")
If something sees the cow then it is kind.
((("something" "sees" "cow" "+")) -> ("something" "is" "kind" "+"))
If something is blue and it likes the cow then it is cold.
((("something" "is" "blue" "+") ("something" "likes" "cow" "+")) -> ("something" "is" "cold" "+"))
If something is green then it needs the lion.
((("something" "is" "green" "+")) -> ("something" "needs" "lion" "+"))
If something sees the tiger and the tiger is cold then the tiger sees the cow.
((("something" "sees" "tiger" "+") ("tiger" "is" "cold" "+")) -> ("tiger" "sees" "cow" "+"))
If something likes the lion then it is kind.
((("something" "likes" "lion" "+")) -> ("something" "is" "kind" "+"))
If something is kind and it sees the dog then it likes the cow.
((("something" "is" "kind" "+") ("something" "sees" "dog" "+")) -> ("something" "likes" "cow" "+"))
If something likes the cow then it is blue.
((("something" "likes" "cow" "+")) -> ("something" "is" "blue" "+"))
If something needs the dog and the dog sees the cow then the dog is young.
((("something" "needs" "dog" "+") ("dog" "sees" "cow" "+")) -> ("dog" "is" "young" "+"))
If something needs the dog then it likes the lion.
((("something" "needs" "dog" "+")) -> ("something" "likes" "lion" "+"))
The tiger likes the dog.
True
1
proof
[(triple11)]
("tiger" "likes" "dog" "+")
triple11
The lion does not see the cow.
False
1
inv-proof
[(triple10)]
("lion" "sees" "cow" "-")
triple10
The cow likes the lion.
True
2
proof
[(((triple3) -> rule9))]
("cow" "likes" "lion" "+")
((triple3) -> (rule9 % int1))
The cow likes the lion.
("cow" "likes" "lion" "+")
int1
The tiger does not like the lion.
False
2
inv-proof
[(((triple12) -> rule9))]
("tiger" "likes" "lion" "-")
((triple12) -> (rule9 % int1))
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int1
The tiger is kind.
True
3
proof
[(((((triple12) -> rule9)) -> rule5))]
("tiger" "is" "kind" "+")
((((triple12) -> (rule9 % int2))) -> (rule5 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int2
The cow is not kind.
False
3
inv-proof
[(((((triple3) -> rule9)) -> rule5))]
("cow" "is" "kind" "-")
((((triple3) -> (rule9 % int2))) -> (rule5 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow likes the lion.
("cow" "likes" "lion" "+")
int2
The tiger likes the cow.
True
5
proof
[(((((((triple12) -> rule9)) -> rule5) triple13) -> rule6))]
("tiger" "likes" "cow" "+")
((((((triple12) -> (rule9 % int3))) -> (rule5 % int2)) triple13) -> (rule6 % int1))
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int3
The cow does not like the cow.
False
5
inv-proof
[(((((((triple3) -> rule9)) -> rule5) triple4) -> rule6))]
("cow" "likes" "cow" "-")
((((((triple3) -> (rule9 % int3))) -> (rule5 % int2)) triple4) -> (rule6 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The cow likes the lion.
("cow" "likes" "lion" "+")
int3
The cow is blue.
True
6
proof
[(((((((((triple3) -> rule9)) -> rule5) triple4) -> rule6)) -> rule7))]
("cow" "is" "blue" "+")
((((((((triple3) -> (rule9 % int4))) -> (rule5 % int3)) triple4) -> (rule6 % int2))) -> (rule7 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2
The cow is kind.
("cow" "is" "kind" "+")
int3
The cow likes the lion.
("cow" "likes" "lion" "+")
int4
The tiger is not blue.
False
6
inv-proof
[(((((((((triple12) -> rule9)) -> rule5) triple13) -> rule6)) -> rule7))]
("tiger" "is" "blue" "-")
((((((((triple12) -> (rule9 % int4))) -> (rule5 % int3)) triple13) -> (rule6 % int2))) -> (rule7 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
int3
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int4
The tiger is cold.
True
12
proof
[(((((((((((triple12) -> rule9)) -> rule5) triple13) -> rule6)) -> rule7) ((((((triple12) -> rule9)) -> rule5) triple13) -> rule6)) -> rule2))]
("tiger" "is" "cold" "+")
((((((((((triple12) -> (rule9 % int5))) -> (rule5 % int4)) triple13) -> (rule6 % int3))) -> (rule7 % int2)) ((((((triple12) -> (rule9 % int5))) -> (rule5 % int4)) triple13) -> (rule6 % int3))) -> (rule2 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int3
The tiger is kind.
("tiger" "is" "kind" "+")
int4
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int5
The tiger is not cold.
False
12
inv-proof
[(((((((((((triple12) -> rule9)) -> rule5) triple13) -> rule6)) -> rule7) ((((((triple12) -> rule9)) -> rule5) triple13) -> rule6)) -> rule2))]
("tiger" "is" "cold" "-")
((((((((((triple12) -> (rule9 % int5))) -> (rule5 % int4)) triple13) -> (rule6 % int3))) -> (rule7 % int2)) ((((((triple12) -> (rule9 % int5))) -> (rule5 % int4)) triple13) -> (rule6 % int3))) -> (rule2 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int3
The tiger is kind.
("tiger" "is" "kind" "+")
int4
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int5
The dog does not need the lion.
Unknown
inv-rconc
[@1: The dog needs the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "needs" "lion" "-")
The tiger needs the lion.
Unknown
rconc
[@1: The tiger needs the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "needs" "lion" "+")
The dog is not blue.
Unknown
inv-rconc
[@2: The dog is blue.[CWA. Example of deepest failure = (rule7 <- rule6 <- FAIL)]]
("dog" "is" "blue" "-")
The lion likes the cow.
Unknown
rconc
[@1: The lion likes the cow.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "likes" "cow" "+")
The dog is not young.
Unknown
inv-rconc
[@1: The dog is young.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("dog" "is" "young" "-")
The tiger sees the cow.
Unknown
rconc
[@1: The tiger sees the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "sees" "cow" "+")
The lion does not need the cow.
Unknown
inv-random
[@0: The lion needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "cow" "-")
The tiger is green.
Unknown
random
[@0: The tiger is green.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "green" "+")
The cow does not need the tiger.
Unknown
inv-random
[@0: The cow needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "tiger" "-")
The cow sees the cow.
Unknown
random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "+")
The lion does not see the lion.
Unknown
inv-random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "-")
The dog sees the tiger.
Unknown
random
[@0: The dog sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "tiger" "+")
@0: The cow is cold.[(triple1 OR ((((((((((triple3) -> rule9)) -> rule5) triple4) -> rule6)) -> rule7) ((((((triple3) -> rule9)) -> rule5) triple4) -> rule6)) -> rule2))] The cow likes the tiger.[(triple2)] The cow needs the dog.[(triple3)] The cow sees the dog.[(triple4)] The dog likes the tiger.[(triple5)] The lion is blue.[(triple6)] The lion is green.[(triple7)] The lion likes the dog.[(triple8)] The lion likes the tiger.[(triple9)] The lion sees the cow.[(triple10)] The tiger likes the dog.[(triple11)] The tiger needs the dog.[(triple12)] The tiger sees the dog.[(triple13)] The tiger sees the lion.[(triple14)] @1: The cow likes the lion.[(((triple3) -> rule9))] The lion is kind.[(((triple10) -> rule1))] The lion needs the lion.[(((triple7) -> rule3))] The tiger likes the lion.[(((triple12) -> rule9))] @2: The cow is kind.[(((((triple3) -> rule9)) -> rule5))] The tiger is kind.[(((((triple12) -> rule9)) -> rule5))] @3: The cow likes the cow.[(((((((triple3) -> rule9)) -> rule5) triple4) -> rule6))] The tiger likes the cow.[(((((((triple12) -> rule9)) -> rule5) triple13) -> rule6))] @4: The cow is blue.[(((((((((triple3) -> rule9)) -> rule5) triple4) -> rule6)) -> rule7))] The tiger is blue.[(((((((((triple12) -> rule9)) -> rule5) triple13) -> rule6)) -> rule7))] @5: The tiger is cold.[(((((((((((triple12) -> rule9)) -> rule5) triple13) -> rule6)) -> rule7) ((((((triple12) -> rule9)) -> rule5) triple13) -> rule6)) -> rule2))]
The cow is cold.
("cow" "is" "cold" "+")
triple1
((((((((((triple3) -> (rule9 % int5))) -> (rule5 % int4)) triple4) -> (rule6 % int3))) -> (rule7 % int2)) ((((((triple3) -> (rule9 % int5))) -> (rule5 % int4)) triple4) -> (rule6 % int3))) -> (rule2 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow likes the cow.
("cow" "likes" "cow" "+")
int3
The cow is kind.
("cow" "is" "kind" "+")
int4
The cow likes the lion.
("cow" "likes" "lion" "+")
int5
The cow likes the tiger.
("cow" "likes" "tiger" "+")
triple2
The cow needs the dog.
("cow" "needs" "dog" "+")
triple3
The cow sees the dog.
("cow" "sees" "dog" "+")
triple4
The dog likes the tiger.
("dog" "likes" "tiger" "+")
triple5
The lion is blue.
("lion" "is" "blue" "+")
triple6
The lion is green.
("lion" "is" "green" "+")
triple7
The lion likes the dog.
("lion" "likes" "dog" "+")
triple8
The lion likes the tiger.
("lion" "likes" "tiger" "+")
triple9
The lion sees the cow.
("lion" "sees" "cow" "+")
triple10
The tiger likes the dog.
("tiger" "likes" "dog" "+")
triple11
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple12
The tiger sees the dog.
("tiger" "sees" "dog" "+")
triple13
The tiger sees the lion.
("tiger" "sees" "lion" "+")
triple14
The cow likes the lion.
("cow" "likes" "lion" "+")
((triple3) -> (rule9 % int1))
The cow likes the lion.
("cow" "likes" "lion" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
((triple10) -> (rule1 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
((triple7) -> (rule3 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The tiger likes the lion.
("tiger" "likes" "lion" "+")
((triple12) -> (rule9 % int1))
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
((((triple3) -> (rule9 % int2))) -> (rule5 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow likes the lion.
("cow" "likes" "lion" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
((((triple12) -> (rule9 % int2))) -> (rule5 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int2
The cow likes the cow.
("cow" "likes" "cow" "+")
((((((triple3) -> (rule9 % int3))) -> (rule5 % int2)) triple4) -> (rule6 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The cow likes the lion.
("cow" "likes" "lion" "+")
int3
The tiger likes the cow.
("tiger" "likes" "cow" "+")
((((((triple12) -> (rule9 % int3))) -> (rule5 % int2)) triple13) -> (rule6 % int1))
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int3
The cow is blue.
("cow" "is" "blue" "+")
((((((((triple3) -> (rule9 % int4))) -> (rule5 % int3)) triple4) -> (rule6 % int2))) -> (rule7 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2
The cow is kind.
("cow" "is" "kind" "+")
int3
The cow likes the lion.
("cow" "likes" "lion" "+")
int4
The tiger is blue.
("tiger" "is" "blue" "+")
((((((((triple12) -> (rule9 % int4))) -> (rule5 % int3)) triple13) -> (rule6 % int2))) -> (rule7 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
int3
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int4
The tiger is cold.
("tiger" "is" "cold" "+")
((((((((((triple12) -> (rule9 % int5))) -> (rule5 % int4)) triple13) -> (rule6 % int3))) -> (rule7 % int2)) ((((((triple12) -> (rule9 % int5))) -> (rule5 % int4)) triple13) -> (rule6 % int3))) -> (rule2 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int3
The tiger is kind.
("tiger" "is" "kind" "+")
int4
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int5