Anne is blue. Anne is round. Charlie is green. Charlie is not quiet. Charlie is round. Charlie is young. Erin is blue. Erin is quiet. Erin is red. Erin is rough. Fiona is quiet. Fiona is rough. Young things are green. If Anne is green then Anne is quiet. Quiet, green things are blue. If Charlie is green then Charlie is blue. Blue things are young. All blue, quiet things are red. If something is round and not green then it is not rough. If something is blue and not young then it is rough.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is round.
("Anne" "is" "round" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Young things are green.
((("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
If Anne is green then Anne is quiet.
((("Anne" "is" "green" "+")) -> ("Anne" "is" "quiet" "+"))
Quiet, green things are blue.
((("something" "is" "quiet" "+") ("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
If Charlie is green then Charlie is blue.
((("Charlie" "is" "green" "+")) -> ("Charlie" "is" "blue" "+"))
Blue things are young.
((("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
All blue, quiet things are red.
((("something" "is" "blue" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "red" "+"))
If something is round and not green then it is not rough.
((("something" "is" "round" "+") ("something" "is" "green" "~")) -> ("something" "is" "rough" "-"))
If something is blue and not young then it is rough.
((("something" "is" "blue" "+") ("something" "is" "young" "~")) -> ("something" "is" "rough" "+"))
Charlie is young.
True
1
proof
[(triple6 OR ((((triple3) -> rule4)) -> rule5))]
("Charlie" "is" "young" "+")
triple6
((((triple3) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is not round.
False
1
inv-proof
[(triple5)]
("Charlie" "is" "round" "-")
triple5
Anne is young.
True
2
proof
[(((triple1) -> rule5))]
("Anne" "is" "young" "+")
((triple1) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Erin is not young.
False
2
inv-proof
[(((triple7) -> rule5))]
("Erin" "is" "young" "-")
((triple7) -> (rule5 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is green.
True
3
proof
[(((((triple7) -> rule5)) -> rule1))]
("Erin" "is" "green" "+")
((((triple7) -> (rule5 % int2))) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Anne is not green.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule1))]
("Anne" "is" "green" "-")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is quiet.
True
4
proof
[(((((((triple1) -> rule5)) -> rule1)) -> rule2))]
("Anne" "is" "quiet" "+")
((((((triple1) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is not quiet.
False
4
inv-proof
[(((((((triple1) -> rule5)) -> rule1)) -> rule2))]
("Anne" "is" "quiet" "-")
((((((triple1) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is not rough.
Unknown
inv-rconc
[@1: Anne is rough.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Anne" "is" "rough" "-")
Charlie is red.
Unknown
rconc
[@1: Charlie is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "red" "+")
Fiona is not young.
Unknown
inv-rconc
[@3: Fiona is young.[CWA. Example of deepest failure = (rule5 <- rule3 <- rule1 <- FAIL)]]
("Fiona" "is" "young" "-")
Fiona is blue.
Unknown
rconc
[@3: Fiona is blue.[CWA. Example of deepest failure = (rule3 <- rule1 <- rule5 <- FAIL)]]
("Fiona" "is" "blue" "+")
Erin is not round.
Unknown
inv-random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "-")
Fiona is round.
Unknown
random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "+")
@0: Anne is blue.[(triple1)] Anne is round.[(triple2)] Charlie is green.[(triple3 OR ((triple6) -> rule1))] Charlie is not quiet.[(triple4)] Charlie is round.[(triple5)] Charlie is young.[(triple6 OR ((((triple3) -> rule4)) -> rule5))] Erin is blue.[(triple7)] Erin is quiet.[(triple8)] Erin is red.[(triple9 OR ((triple7 triple8) -> rule6))] Erin is rough.[(triple10)] Fiona is quiet.[(triple11)] Fiona is rough.[(triple12)] @1: Anne is young.[(((triple1) -> rule5))] Charlie is blue.[(((triple3) -> rule4) OR ((((triple6) -> rule1)) -> rule4))] Erin is young.[(((triple7) -> rule5))] @2: Anne is green.[(((((triple1) -> rule5)) -> rule1))] Erin is green.[(((((triple7) -> rule5)) -> rule1))] @3: Anne is quiet.[(((((((triple1) -> rule5)) -> rule1)) -> rule2))] @4: Anne is red.[(((triple1 ((((((triple1) -> rule5)) -> rule1)) -> rule2)) -> rule6))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is round.
("Anne" "is" "round" "+")
triple2
Charlie is green.
("Charlie" "is" "green" "+")
triple3
((triple6) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
triple4
Charlie is round.
("Charlie" "is" "round" "+")
triple5
Charlie is young.
("Charlie" "is" "young" "+")
triple6
((((triple3) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
triple7
Erin is quiet.
("Erin" "is" "quiet" "+")
triple8
Erin is red.
("Erin" "is" "red" "+")
triple9
((triple7 triple8) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
triple10
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple11
Fiona is rough.
("Fiona" "is" "rough" "+")
triple12
Anne is young.
("Anne" "is" "young" "+")
((triple1) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple3) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((((triple6) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
((triple7) -> (rule5 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
((((triple7) -> (rule5 % int2))) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
((((((triple1) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
((triple1 ((((((triple1) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4