The cow is cold. If someone is big then they are young. Young, blue people are not cold. If someone is cold then they are big. If the cow is young and the cow is blue then the cow is cold. If someone is blue and not big then they are rough. All young people are rough.
The cow is cold.
("cow" "is" "cold" "+")
If someone is big then they are young.
((("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
Young, blue people are not cold.
((("someone" "is" "young" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "-"))
If someone is cold then they are big.
((("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
If the cow is young and the cow is blue then the cow is cold.
((("cow" "is" "young" "+") ("cow" "is" "blue" "+")) -> ("cow" "is" "cold" "+"))
If someone is blue and not big then they are rough.
((("someone" "is" "blue" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "rough" "+"))
All young people are rough.
((("someone" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
The cow is cold.
True
1
proof
[(triple1)]
("cow" "is" "cold" "+")
triple1
The cow is not cold.
False
1
inv-proof
[(triple1)]
("cow" "is" "cold" "-")
triple1
The cow is big.
True
2
proof
[(((triple1) -> rule3))]
("cow" "is" "big" "+")
((triple1) -> (rule3 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is not big.
False
2
inv-proof
[(((triple1) -> rule3))]
("cow" "is" "big" "-")
((triple1) -> (rule3 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is young.
True
3
proof
[(((((triple1) -> rule3)) -> rule1))]
("cow" "is" "young" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The cow is not young.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule1))]
("cow" "is" "young" "-")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The cow is rough.
True
4
proof
[(((((((triple1) -> rule3)) -> rule1)) -> rule6))]
("cow" "is" "rough" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is big.
("cow" "is" "big" "+")
int3
The cow is not rough.
False
4
inv-proof
[(((((((triple1) -> rule3)) -> rule1)) -> rule6))]
("cow" "is" "rough" "-")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is big.
("cow" "is" "big" "+")
int3
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 is blue.
Unknown
random
[@0: The cow is blue.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "blue" "+")
The cow does not visit the cow.
Unknown
inv-random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "-")
The cow likes the cow.
Unknown
random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cow" "+")
@0: The cow is cold.[(triple1)] @1: The cow is big.[(((triple1) -> rule3))] @2: The cow is young.[(((((triple1) -> rule3)) -> rule1))] @3: The cow is rough.[(((((((triple1) -> rule3)) -> rule1)) -> rule6))]
The cow is cold.
("cow" "is" "cold" "+")
triple1
The cow is big.
("cow" "is" "big" "+")
((triple1) -> (rule3 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is young.
("cow" "is" "young" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The cow is rough.
("cow" "is" "rough" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is big.
("cow" "is" "big" "+")
int3