Anne is white. Charlie is nice. Fiona is blue. Green things are quiet. Red things are green. Nice, green things are young. If Charlie is green and Charlie is white then Charlie is young. If something is quiet and blue then it is young. Blue things are green.
Anne is white.
("Anne" "is" "white" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Green things are quiet.
((("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
Red things are green.
((("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
Nice, green things are young.
((("something" "is" "nice" "+") ("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
If Charlie is green and Charlie is white then Charlie is young.
((("Charlie" "is" "green" "+") ("Charlie" "is" "white" "+")) -> ("Charlie" "is" "young" "+"))
If something is quiet and blue then it is young.
((("something" "is" "quiet" "+") ("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
Blue things are green.
((("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
Charlie is nice.
True
1
proof
[(triple2)]
("Charlie" "is" "nice" "+")
triple2
Charlie is not nice.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "nice" "-")
triple2
Fiona is green.
True
2
proof
[(((triple3) -> rule6))]
("Fiona" "is" "green" "+")
((triple3) -> (rule6 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is not green.
False
2
inv-proof
[(((triple3) -> rule6))]
("Fiona" "is" "green" "-")
((triple3) -> (rule6 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is quiet.
True
3
proof
[(((((triple3) -> rule6)) -> rule1))]
("Fiona" "is" "quiet" "+")
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is not quiet.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule1))]
("Fiona" "is" "quiet" "-")
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is young.
True
5
proof
[(((((((triple3) -> rule6)) -> rule1) triple3) -> rule5))]
("Fiona" "is" "young" "+")
((((((triple3) -> (rule6 % int3))) -> (rule1 % int2)) triple3) -> (rule5 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Fiona is not young.
False
5
inv-proof
[(((((((triple3) -> rule6)) -> rule1) triple3) -> rule5))]
("Fiona" "is" "young" "-")
((((((triple3) -> (rule6 % int3))) -> (rule1 % int2)) triple3) -> (rule5 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Anne is not young.
Unknown
inv-rconc
[@1: Anne is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "young" "-")
Charlie is quiet.
Unknown
rconc
[@2: Charlie is quiet.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Charlie" "is" "quiet" "+")
Charlie is not young.
Unknown
inv-rconc
[@2: Charlie is young.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Charlie" "is" "young" "-")
Charlie is green.
Unknown
rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "green" "+")
Anne is not red.
Unknown
inv-random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
Anne is not nice.
Unknown
inv-random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
@0: Anne is white.[(triple1)] Charlie is nice.[(triple2)] Fiona is blue.[(triple3)] @1: Fiona is green.[(((triple3) -> rule6))] @2: Fiona is quiet.[(((((triple3) -> rule6)) -> rule1))] @3: Fiona is young.[(((((((triple3) -> rule6)) -> rule1) triple3) -> rule5))]
Anne is white.
("Anne" "is" "white" "+")
triple1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
Fiona is blue.
("Fiona" "is" "blue" "+")
triple3
Fiona is green.
("Fiona" "is" "green" "+")
((triple3) -> (rule6 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
((((((triple3) -> (rule6 % int3))) -> (rule1 % int2)) triple3) -> (rule5 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3