Anne is big. Anne is blue. Anne is nice. Charlie is big. Charlie is young. Gary is big. Gary is round. If something is green then it is young. All big things are green. If something is young then it is nice.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is round.
("Gary" "is" "round" "+")
If something is green then it is young.
((("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
All big things are green.
((("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
If something is young then it is nice.
((("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
Anne is blue.
True
1
proof
[(triple2)]
("Anne" "is" "blue" "+")
triple2
Anne is not blue.
False
1
inv-proof
[(triple2)]
("Anne" "is" "blue" "-")
triple2
Gary is green.
True
2
proof
[(((triple6) -> rule2))]
("Gary" "is" "green" "+")
((triple6) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Anne is not green.
False
2
inv-proof
[(((triple1) -> rule2))]
("Anne" "is" "green" "-")
((triple1) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Gary is young.
True
3
proof
[(((((triple6) -> rule2)) -> rule1))]
("Gary" "is" "young" "+")
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is not young.
False
3
inv-proof
[(((((triple6) -> rule2)) -> rule1))]
("Gary" "is" "young" "-")
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is nice.
True
4
proof
[(((((((triple6) -> rule2)) -> rule1)) -> rule3))]
("Gary" "is" "nice" "+")
((((((triple6) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is not nice.
False
4
inv-proof
[(((((((triple6) -> rule2)) -> rule1)) -> rule3))]
("Gary" "is" "nice" "-")
((((((triple6) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Anne is not rough.
Unknown
inv-random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
Anne is not round.
Unknown
inv-random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
@0: Anne is big.[(triple1)] Anne is blue.[(triple2)] Anne is nice.[(triple3 OR ((((((triple1) -> rule2)) -> rule1)) -> rule3))] Charlie is big.[(triple4)] Charlie is young.[(triple5 OR ((((triple4) -> rule2)) -> rule1))] Gary is big.[(triple6)] Gary is round.[(triple7)] @1: Anne is green.[(((triple1) -> rule2))] Charlie is green.[(((triple4) -> rule2))] Charlie is nice.[(((triple5) -> rule3) OR ((((((triple4) -> rule2)) -> rule1)) -> rule3))] Gary is green.[(((triple6) -> rule2))] @2: Anne is young.[(((((triple1) -> rule2)) -> rule1))] Gary is young.[(((((triple6) -> rule2)) -> rule1))] @3: Gary is nice.[(((((((triple6) -> rule2)) -> rule1)) -> rule3))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is nice.
("Anne" "is" "nice" "+")
triple3
((((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
triple4
Charlie is young.
("Charlie" "is" "young" "+")
triple5
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
triple6
Gary is round.
("Gary" "is" "round" "+")
triple7
Anne is green.
("Anne" "is" "green" "+")
((triple1) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
((triple4) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple5) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((((((triple4) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
((triple6) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
((((((triple6) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3