Anne is round. Anne is smart. Anne is young. Dave is green. Dave is not rough. Erin is not white. Fiona is not round. All round, green things are rough. All red things are not young. Round things are green. If Dave is young and Dave is rough then Dave is white. If Erin is round then Erin is smart. If something is rough and young then it is not white.
Anne is round.
("Anne" "is" "round" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is young.
("Anne" "is" "young" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is not rough.
("Dave" "is" "rough" "-")
Erin is not white.
("Erin" "is" "white" "-")
Fiona is not round.
("Fiona" "is" "round" "-")
All round, green things are rough.
((("something" "is" "round" "+") ("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
All red things are not young.
((("something" "is" "red" "+")) -> ("something" "is" "young" "-"))
Round things are green.
((("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
If Dave is young and Dave is rough then Dave is white.
((("Dave" "is" "young" "+") ("Dave" "is" "rough" "+")) -> ("Dave" "is" "white" "+"))
If Erin is round then Erin is smart.
((("Erin" "is" "round" "+")) -> ("Erin" "is" "smart" "+"))
If something is rough and young then it is not white.
((("something" "is" "rough" "+") ("something" "is" "young" "+")) -> ("something" "is" "white" "-"))
Dave is green.
True
1
proof
[(triple4)]
("Dave" "is" "green" "+")
triple4
Anne is not round.
False
1
inv-proof
[(triple1)]
("Anne" "is" "round" "-")
triple1
Anne is green.
True
2
proof
[(((triple1) -> rule3))]
("Anne" "is" "green" "+")
((triple1) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is not green.
False
2
inv-proof
[(((triple1) -> rule3))]
("Anne" "is" "green" "-")
((triple1) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is rough.
True
4
proof
[(((triple1 ((triple1) -> rule3)) -> rule1))]
("Anne" "is" "rough" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is not rough.
False
4
inv-proof
[(((triple1 ((triple1) -> rule3)) -> rule1))]
("Anne" "is" "rough" "-")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is not white.
True
6
proof
[(((((triple1 ((triple1) -> rule3)) -> rule1) triple3) -> rule6))]
("Anne" "is" "white" "-")
((((triple1 ((triple1) -> (rule3 % int3))) -> (rule1 % int2)) triple3) -> (rule6 % int1))
Anne is not white.
("Anne" "is" "white" "-")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is white.
False
6
inv-proof
[(((((triple1 ((triple1) -> rule3)) -> rule1) triple3) -> rule6))]
("Anne" "is" "white" "+")
((((triple1 ((triple1) -> (rule3 % int3))) -> (rule1 % int2)) triple3) -> (rule6 % int1))
Anne is not white.
("Anne" "is" "white" "-")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Fiona is not rough.
Unknown
inv-rconc
[@1: Fiona is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "rough" "-")
Fiona is green.
Unknown
rconc
[@1: Fiona is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "green" "+")
Erin is not green.
Unknown
inv-rconc
[@1: Erin is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "green" "-")
Erin is rough.
Unknown
rconc
[@1: Erin is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "rough" "+")
Dave is not round.
Unknown
inv-random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "-")
Erin is young.
Unknown
random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "+")
Dave is not smart.
Unknown
inv-random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "-")
Erin is red.
Unknown
random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "+")
@0: Anne is round.[(triple1)] Anne is smart.[(triple2)] Anne is young.[(triple3)] Dave is green.[(triple4)] Dave is not rough.[(triple5)] Erin is not white.[(triple6)] Fiona is not round.[(triple7)] @1: Anne is green.[(((triple1) -> rule3))] @2: Anne is rough.[(((triple1 ((triple1) -> rule3)) -> rule1))] @3: Anne is not white.[(((((triple1 ((triple1) -> rule3)) -> rule1) triple3) -> rule6))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Anne is smart.
("Anne" "is" "smart" "+")
triple2
Anne is young.
("Anne" "is" "young" "+")
triple3
Dave is green.
("Dave" "is" "green" "+")
triple4
Dave is not rough.
("Dave" "is" "rough" "-")
triple5
Erin is not white.
("Erin" "is" "white" "-")
triple6
Fiona is not round.
("Fiona" "is" "round" "-")
triple7
Anne is green.
("Anne" "is" "green" "+")
((triple1) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is not white.
("Anne" "is" "white" "-")
((((triple1 ((triple1) -> (rule3 % int3))) -> (rule1 % int2)) triple3) -> (rule6 % int1))
Anne is not white.
("Anne" "is" "white" "-")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3