Erin is big. If Erin is young and Erin is kind then Erin is nice. All big things are kind. If something is big and round then it is young. All round things are big. All young, rough things are big. If something is green and nice then it is round. Kind things are young. If something is rough then it is green.
Erin is big.
("Erin" "is" "big" "+")
If Erin is young and Erin is kind then Erin is nice.
((("Erin" "is" "young" "+") ("Erin" "is" "kind" "+")) -> ("Erin" "is" "nice" "+"))
All big things are kind.
((("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
If something is big and round then it is young.
((("something" "is" "big" "+") ("something" "is" "round" "+")) -> ("something" "is" "young" "+"))
All round things are big.
((("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
All young, rough things are big.
((("something" "is" "young" "+") ("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
If something is green and nice then it is round.
((("something" "is" "green" "+") ("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
Kind things are young.
((("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
If something is rough then it is green.
((("something" "is" "rough" "+")) -> ("something" "is" "green" "+"))
Erin is big.
True
1
proof
[(triple1)]
("Erin" "is" "big" "+")
triple1
Erin is not big.
False
1
inv-proof
[(triple1)]
("Erin" "is" "big" "-")
triple1
Erin is kind.
True
2
proof
[(((triple1) -> rule2))]
("Erin" "is" "kind" "+")
((triple1) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is not kind.
False
2
inv-proof
[(((triple1) -> rule2))]
("Erin" "is" "kind" "-")
((triple1) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is young.
True
3
proof
[(((((triple1) -> rule2)) -> rule7))]
("Erin" "is" "young" "+")
((((triple1) -> (rule2 % int2))) -> (rule7 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is not young.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule7))]
("Erin" "is" "young" "-")
((((triple1) -> (rule2 % int2))) -> (rule7 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is not round.
Unknown
inv-rconc
[@2: Erin is round.[CWA. Example of deepest failure = (rule6 <- rule8 <- FAIL)]]
("Erin" "is" "round" "-")
Erin is green.
Unknown
rconc
[@1: Erin is green.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Erin" "is" "green" "+")
@0: Erin is big.[(triple1)] @1: Erin is kind.[(((triple1) -> rule2))] @2: Erin is young.[(((((triple1) -> rule2)) -> rule7))] @3: Erin is nice.[(((((((triple1) -> rule2)) -> rule7) ((triple1) -> rule2)) -> rule1))]
Erin is big.
("Erin" "is" "big" "+")
triple1
Erin is kind.
("Erin" "is" "kind" "+")
((triple1) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
((((triple1) -> (rule2 % int2))) -> (rule7 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
((((((triple1) -> (rule2 % int3))) -> (rule7 % int2)) ((triple1) -> (rule2 % int3))) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3