Anne is smart. Charlie is rough. Erin is smart. Fiona is red. If Fiona is rough then Fiona is furry. If Erin is nice then Erin is smart. Red things are smart. Nice things are furry. Smart things are green. All green things are young.
Anne is smart.
("Anne" "is" "smart" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Fiona is red.
("Fiona" "is" "red" "+")
If Fiona is rough then Fiona is furry.
((("Fiona" "is" "rough" "+")) -> ("Fiona" "is" "furry" "+"))
If Erin is nice then Erin is smart.
((("Erin" "is" "nice" "+")) -> ("Erin" "is" "smart" "+"))
Red things are smart.
((("something" "is" "red" "+")) -> ("something" "is" "smart" "+"))
Nice things are furry.
((("something" "is" "nice" "+")) -> ("something" "is" "furry" "+"))
Smart things are green.
((("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
All green things are young.
((("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
Erin is smart.
True
1
proof
[(triple3)]
("Erin" "is" "smart" "+")
triple3
Fiona is not red.
False
1
inv-proof
[(triple4)]
("Fiona" "is" "red" "-")
triple4
Fiona is smart.
True
2
proof
[(((triple4) -> rule3))]
("Fiona" "is" "smart" "+")
((triple4) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Erin is not green.
False
2
inv-proof
[(((triple3) -> rule5))]
("Erin" "is" "green" "-")
((triple3) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is young.
True
3
proof
[(((((triple3) -> rule5)) -> rule6))]
("Erin" "is" "young" "+")
((((triple3) -> (rule5 % int2))) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Fiona is not green.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule5))]
("Fiona" "is" "green" "-")
((((triple4) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is young.
True
4
proof
[(((((((triple4) -> rule3)) -> rule5)) -> rule6))]
("Fiona" "is" "young" "+")
((((((triple4) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is not young.
False
4
inv-proof
[(((((((triple4) -> rule3)) -> rule5)) -> rule6))]
("Fiona" "is" "young" "-")
((((((triple4) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is not furry.
Unknown
inv-rconc
[@1: Fiona is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "furry" "-")
Anne is furry.
Unknown
rconc
[@1: Anne is furry.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "furry" "+")
Charlie is not young.
Unknown
inv-rconc
[@3: Charlie is young.[CWA. Example of deepest failure = (rule6 <- rule5 <- rule3 <- FAIL)]]
("Charlie" "is" "young" "-")
Charlie is smart.
Unknown
rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "smart" "+")
Charlie is not nice.
Unknown
inv-random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "-")
Anne is red.
Unknown
random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "+")
Erin is not nice.
Unknown
inv-random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "-")
Fiona is nice.
Unknown
random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "+")
@0: Anne is smart.[(triple1)] Charlie is rough.[(triple2)] Erin is smart.[(triple3)] Fiona is red.[(triple4)] @1: Anne is green.[(((triple1) -> rule5))] Erin is green.[(((triple3) -> rule5))] Fiona is smart.[(((triple4) -> rule3))] @2: Anne is young.[(((((triple1) -> rule5)) -> rule6))] Erin is young.[(((((triple3) -> rule5)) -> rule6))] Fiona is green.[(((((triple4) -> rule3)) -> rule5))] @3: Fiona is young.[(((((((triple4) -> rule3)) -> rule5)) -> rule6))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple2
Erin is smart.
("Erin" "is" "smart" "+")
triple3
Fiona is red.
("Fiona" "is" "red" "+")
triple4
Anne is green.
("Anne" "is" "green" "+")
((triple1) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
((triple3) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple4) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
((((triple3) -> (rule5 % int2))) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
((((triple4) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
((((((triple4) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3