Erin is blue. If Erin is big and Erin is green then Erin is rough. If Erin is smart and Erin is rough then Erin is young. If something is big then it is green. White things are big. If something is blue then it is big. If something is big and not white then it is young.
Erin is blue.
("Erin" "is" "blue" "+")
If Erin is big and Erin is green then Erin is rough.
((("Erin" "is" "big" "+") ("Erin" "is" "green" "+")) -> ("Erin" "is" "rough" "+"))
If Erin is smart and Erin is rough then Erin is young.
((("Erin" "is" "smart" "+") ("Erin" "is" "rough" "+")) -> ("Erin" "is" "young" "+"))
If something is big then it is green.
((("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
White things are big.
((("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
If something is blue then it is big.
((("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
If something is big and not white then it is young.
((("something" "is" "big" "+") ("something" "is" "white" "~")) -> ("something" "is" "young" "+"))
Erin is blue.
True
1
proof
[(triple1)]
("Erin" "is" "blue" "+")
triple1
Erin is not blue.
False
1
inv-proof
[(triple1)]
("Erin" "is" "blue" "-")
triple1
Erin is big.
True
2
proof
[(((triple1) -> rule5))]
("Erin" "is" "big" "+")
((triple1) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is not big.
False
2
inv-proof
[(((triple1) -> rule5))]
("Erin" "is" "big" "-")
((triple1) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is green.
True
3
proof
[(((((triple1) -> rule5)) -> rule3))]
("Erin" "is" "green" "+")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is not green.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule3))]
("Erin" "is" "green" "-")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is rough.
True
6
proof
[(((((triple1) -> rule5) ((((triple1) -> rule5)) -> rule3)) -> rule1))]
("Erin" "is" "rough" "+")
((((triple1) -> (rule5 % int3)) ((((triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is not rough.
False
6
inv-proof
[(((((triple1) -> rule5) ((((triple1) -> rule5)) -> rule3)) -> rule1))]
("Erin" "is" "rough" "-")
((((triple1) -> (rule5 % int3)) ((((triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is not young.
Unknown
inv-rconc
[@1: Erin is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "young" "-")
Erin is smart.
Unknown
random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "+")
@0: Erin is blue.[(triple1)] @1: Erin is big.[(((triple1) -> rule5))] @2: Erin is green.[(((((triple1) -> rule5)) -> rule3))] @3: Erin is rough.[(((((triple1) -> rule5) ((((triple1) -> rule5)) -> rule3)) -> rule1))]
Erin is blue.
("Erin" "is" "blue" "+")
triple1
Erin is big.
("Erin" "is" "big" "+")
((triple1) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
((((triple1) -> (rule5 % int3)) ((((triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3