The cow chases the tiger. The cow is rough. The cow sees the tiger. The cow visits the rabbit. The cow visits the tiger. The rabbit chases the tiger. The rabbit is blue. The rabbit is kind. The rabbit visits the cow. The tiger is blue. If the cow visits the rabbit then the cow is cold. Kind, rough things are nice. If something is cold then it is kind.
The cow chases the tiger.
("cow" "chases" "tiger" "+")
The cow is rough.
("cow" "is" "rough" "+")
The cow sees the tiger.
("cow" "sees" "tiger" "+")
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
The cow visits the tiger.
("cow" "visits" "tiger" "+")
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
If the cow visits the rabbit then the cow is cold.
((("cow" "visits" "rabbit" "+")) -> ("cow" "is" "cold" "+"))
Kind, rough things are nice.
((("something" "is" "kind" "+") ("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
If something is cold then it is kind.
((("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
The rabbit is blue.
True
1
proof
[(triple7)]
("rabbit" "is" "blue" "+")
triple7
The rabbit does not visit the cow.
False
1
inv-proof
[(triple9)]
("rabbit" "visits" "cow" "-")
triple9
The cow is cold.
True
2
proof
[(((triple4) -> rule1))]
("cow" "is" "cold" "+")
((triple4) -> (rule1 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is not cold.
False
2
inv-proof
[(((triple4) -> rule1))]
("cow" "is" "cold" "-")
((triple4) -> (rule1 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is kind.
True
3
proof
[(((((triple4) -> rule1)) -> rule3))]
("cow" "is" "kind" "+")
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow is not kind.
False
3
inv-proof
[(((((triple4) -> rule1)) -> rule3))]
("cow" "is" "kind" "-")
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow is nice.
True
5
proof
[(((((((triple4) -> rule1)) -> rule3) triple2) -> rule2))]
("cow" "is" "nice" "+")
((((((triple4) -> (rule1 % int3))) -> (rule3 % int2)) triple2) -> (rule2 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
The cow is not nice.
False
5
inv-proof
[(((((((triple4) -> rule1)) -> rule3) triple2) -> rule2))]
("cow" "is" "nice" "-")
((((((triple4) -> (rule1 % int3))) -> (rule3 % int2)) triple2) -> (rule2 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
The tiger is not kind.
Unknown
inv-rconc
[@1: The tiger is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "is" "kind" "-")
The tiger is nice.
Unknown
rconc
[@1: The tiger is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "is" "nice" "+")
The rabbit is not nice.
Unknown
inv-rconc
[@1: The rabbit is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "is" "nice" "-")
The tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
The rabbit is not rough.
Unknown
inv-random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "-")
The tiger chases the cow.
Unknown
random
[@0: The tiger chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "cow" "+")
The tiger is not rough.
Unknown
inv-random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "-")
The tiger visits the rabbit.
Unknown
random
[@0: The tiger visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "rabbit" "+")
@0: The cow chases the tiger.[(triple1)] The cow is rough.[(triple2)] The cow sees the tiger.[(triple3)] The cow visits the rabbit.[(triple4)] The cow visits the tiger.[(triple5)] The rabbit chases the tiger.[(triple6)] The rabbit is blue.[(triple7)] The rabbit is kind.[(triple8)] The rabbit visits the cow.[(triple9)] The tiger is blue.[(triple10)] @1: The cow is cold.[(((triple4) -> rule1))] @2: The cow is kind.[(((((triple4) -> rule1)) -> rule3))] @3: The cow is nice.[(((((((triple4) -> rule1)) -> rule3) triple2) -> rule2))]
The cow chases the tiger.
("cow" "chases" "tiger" "+")
triple1
The cow is rough.
("cow" "is" "rough" "+")
triple2
The cow sees the tiger.
("cow" "sees" "tiger" "+")
triple3
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
triple4
The cow visits the tiger.
("cow" "visits" "tiger" "+")
triple5
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
triple6
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple7
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple8
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
triple9
The tiger is blue.
("tiger" "is" "blue" "+")
triple10
The cow is cold.
("cow" "is" "cold" "+")
((triple4) -> (rule1 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow is nice.
("cow" "is" "nice" "+")
((((((triple4) -> (rule1 % int3))) -> (rule3 % int2)) triple2) -> (rule2 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3