Charlie is green. Erin is kind. Erin is red. If Erin is young and Erin is kind then Erin is round. All big, red things are young. Kind things are big.
Charlie is green.
("Charlie" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is red.
("Erin" "is" "red" "+")
If Erin is young and Erin is kind then Erin is round.
((("Erin" "is" "young" "+") ("Erin" "is" "kind" "+")) -> ("Erin" "is" "round" "+"))
All big, red things are young.
((("something" "is" "big" "+") ("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
Kind things are big.
((("something" "is" "kind" "+")) -> ("something" "is" "big" "+"))
Erin is red.
True
1
proof
[(triple3)]
("Erin" "is" "red" "+")
triple3
Erin is not red.
False
1
inv-proof
[(triple3)]
("Erin" "is" "red" "-")
triple3
Erin is big.
True
2
proof
[(((triple2) -> rule3))]
("Erin" "is" "big" "+")
((triple2) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is not big.
False
2
inv-proof
[(((triple2) -> rule3))]
("Erin" "is" "big" "-")
((triple2) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is young.
True
4
proof
[(((((triple2) -> rule3) triple3) -> rule2))]
("Erin" "is" "young" "+")
((((triple2) -> (rule3 % int2)) triple3) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is not young.
False
4
inv-proof
[(((((triple2) -> rule3) triple3) -> rule2))]
("Erin" "is" "young" "-")
((((triple2) -> (rule3 % int2)) triple3) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is round.
True
6
proof
[(((((((triple2) -> rule3) triple3) -> rule2) triple2) -> rule1))]
("Erin" "is" "round" "+")
((((((triple2) -> (rule3 % int3)) triple3) -> (rule2 % int2)) triple2) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is not round.
False
6
inv-proof
[(((((((triple2) -> rule3) triple3) -> rule2) triple2) -> rule1))]
("Erin" "is" "round" "-")
((((((triple2) -> (rule3 % int3)) triple3) -> (rule2 % int2)) triple2) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Charlie is not young.
Unknown
inv-rconc
[@1: Charlie is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "young" "-")
Charlie is big.
Unknown
rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "big" "+")
Erin is not green.
Unknown
inv-random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
Charlie is not white.
Unknown
inv-random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
Erin is not white.
Unknown
inv-random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
@0: Charlie is green.[(triple1)] Erin is kind.[(triple2)] Erin is red.[(triple3)] @1: Erin is big.[(((triple2) -> rule3))] @2: Erin is young.[(((((triple2) -> rule3) triple3) -> rule2))] @3: Erin is round.[(((((((triple2) -> rule3) triple3) -> rule2) triple2) -> rule1))]
Charlie is green.
("Charlie" "is" "green" "+")
triple1
Erin is kind.
("Erin" "is" "kind" "+")
triple2
Erin is red.
("Erin" "is" "red" "+")
triple3
Erin is big.
("Erin" "is" "big" "+")
((triple2) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
((((triple2) -> (rule3 % int2)) triple3) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
((((((triple2) -> (rule3 % int3)) triple3) -> (rule2 % int2)) triple2) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3