The cat is rough. All big, round people are rough. All big, red people are rough. Round, red people are rough. If someone is big then they are rough. Big people are round. All rough, cold people are big. If someone is round and red then they are not cold. All rough people are cold.
The cat is rough.
("cat" "is" "rough" "+")
All big, round people are rough.
((("someone" "is" "big" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
All big, red people are rough.
((("someone" "is" "big" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "rough" "+"))
Round, red people are rough.
((("someone" "is" "round" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "rough" "+"))
If someone is big then they are rough.
((("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
Big people are round.
((("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
All rough, cold people are big.
((("someone" "is" "rough" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
If someone is round and red then they are not cold.
((("someone" "is" "round" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "cold" "-"))
All rough people are cold.
((("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
The cat is rough.
True
1
proof
[(triple1)]
("cat" "is" "rough" "+")
triple1
The cat is not rough.
False
1
inv-proof
[(triple1)]
("cat" "is" "rough" "-")
triple1
The cat is cold.
True
2
proof
[(((triple1) -> rule8))]
("cat" "is" "cold" "+")
((triple1) -> (rule8 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is not cold.
False
2
inv-proof
[(((triple1) -> rule8))]
("cat" "is" "cold" "-")
((triple1) -> (rule8 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is big.
True
4
proof
[(((triple1 ((triple1) -> rule8)) -> rule6))]
("cat" "is" "big" "+")
((triple1 ((triple1) -> (rule8 % int2))) -> (rule6 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The cat is not big.
False
4
inv-proof
[(((triple1 ((triple1) -> rule8)) -> rule6))]
("cat" "is" "big" "-")
((triple1 ((triple1) -> (rule8 % int2))) -> (rule6 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The cat is round.
True
5
proof
[(((((triple1 ((triple1) -> rule8)) -> rule6)) -> rule5))]
("cat" "is" "round" "+")
((((triple1 ((triple1) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The cat is cold.
("cat" "is" "cold" "+")
int3
The cat is not round.
False
5
inv-proof
[(((((triple1 ((triple1) -> rule8)) -> rule6)) -> rule5))]
("cat" "is" "round" "-")
((((triple1 ((triple1) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The cat is cold.
("cat" "is" "cold" "+")
int3
The cat is not red.
Unknown
inv-random
[@0: The cat is red.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "red" "-")
The cat needs the cat.
Unknown
random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "+")
The cat does not see the cat.
Unknown
inv-random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "-")
The cat likes the cat.
Unknown
random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "+")
@0: The cat is rough.[(triple1)] @1: The cat is cold.[(((triple1) -> rule8))] @2: The cat is big.[(((triple1 ((triple1) -> rule8)) -> rule6))] @3: The cat is round.[(((((triple1 ((triple1) -> rule8)) -> rule6)) -> rule5))]
The cat is rough.
("cat" "is" "rough" "+")
triple1
The cat is cold.
("cat" "is" "cold" "+")
((triple1) -> (rule8 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is big.
("cat" "is" "big" "+")
((triple1 ((triple1) -> (rule8 % int2))) -> (rule6 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The cat is round.
("cat" "is" "round" "+")
((((triple1 ((triple1) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The cat is cold.
("cat" "is" "cold" "+")
int3