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