The cow is round. If the cow is red and the cow is big then the cow is young. Round things are red. If something is young and round then it is red. If something is big and round then it is red. All young things are big. All blue, red things are young. All red things are young. If something is blue then it is round.
The cow is round.
("cow" "is" "round" "+")
If the cow is red and the cow is big then the cow is young.
((("cow" "is" "red" "+") ("cow" "is" "big" "+")) -> ("cow" "is" "young" "+"))
Round things are red.
((("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
If something is young and round then it is red.
((("something" "is" "young" "+") ("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
If something is big and round then it is red.
((("something" "is" "big" "+") ("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
All young things are big.
((("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
All blue, red things are young.
((("something" "is" "blue" "+") ("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
All red things are young.
((("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
If something is blue then it is round.
((("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
The cow is round.
True
1
proof
[(triple1)]
("cow" "is" "round" "+")
triple1
The cow is not round.
False
1
inv-proof
[(triple1)]
("cow" "is" "round" "-")
triple1
The cow is red.
True
2
proof
[(((triple1) -> rule2))]
("cow" "is" "red" "+")
((triple1) -> (rule2 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is not red.
False
2
inv-proof
[(((triple1) -> rule2))]
("cow" "is" "red" "-")
((triple1) -> (rule2 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is young.
True
3
proof
[(((((triple1) -> rule2)) -> rule7))]
("cow" "is" "young" "+")
((((triple1) -> (rule2 % int2))) -> (rule7 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow is not young.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule7))]
("cow" "is" "young" "-")
((((triple1) -> (rule2 % int2))) -> (rule7 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow is big.
True
4
proof
[(((((((triple1) -> rule2)) -> rule7)) -> rule5))]
("cow" "is" "big" "+")
((((((triple1) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3
The cow is not big.
False
4
inv-proof
[(((((((triple1) -> rule2)) -> rule7)) -> rule5))]
("cow" "is" "big" "-")
((((((triple1) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3
The cow is not blue.
Unknown
inv-random
[@0: The cow is blue.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "blue" "-")
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 visit the cow.
Unknown
inv-random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "-")
The cow eats the cow.
Unknown
random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "+")
@0: The cow is round.[(triple1)] @1: The cow is red.[(((triple1) -> rule2))] @2: The cow is young.[(((((triple1) -> rule2)) -> rule7))] @3: The cow is big.[(((((((triple1) -> rule2)) -> rule7)) -> rule5))]
The cow is round.
("cow" "is" "round" "+")
triple1
The cow is red.
("cow" "is" "red" "+")
((triple1) -> (rule2 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is young.
("cow" "is" "young" "+")
((((triple1) -> (rule2 % int2))) -> (rule7 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow is big.
("cow" "is" "big" "+")
((((((triple1) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3