Erin is young. Quiet things are young. All big things are rough. If something is young and quiet then it is not big. Young things are quiet. All big things are quiet. If something is quiet and not big then it is cold. If something is quiet and not white then it is cold. If Erin is not cold then Erin is rough.
Erin is young.
("Erin" "is" "young" "+")
Quiet things are young.
((("something" "is" "quiet" "+")) -> ("something" "is" "young" "+"))
All big things are rough.
((("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
If something is young and quiet then it is not big.
((("something" "is" "young" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "big" "-"))
Young things are quiet.
((("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
All big things are quiet.
((("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
If something is quiet and not big then it is cold.
((("something" "is" "quiet" "+") ("something" "is" "big" "~")) -> ("something" "is" "cold" "+"))
If something is quiet and not white then it is cold.
((("something" "is" "quiet" "+") ("something" "is" "white" "~")) -> ("something" "is" "cold" "+"))
If Erin is not cold then Erin is rough.
((("Erin" "is" "cold" "~")) -> ("Erin" "is" "rough" "+"))
Erin is young.
True
1
proof
[(triple1)]
("Erin" "is" "young" "+")
triple1
Erin is not young.
False
1
inv-proof
[(triple1)]
("Erin" "is" "young" "-")
triple1
Erin is quiet.
True
2
proof
[(((triple1) -> rule4))]
("Erin" "is" "quiet" "+")
((triple1) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is not quiet.
False
2
inv-proof
[(((triple1) -> rule4))]
("Erin" "is" "quiet" "-")
((triple1) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is not big.
True
4
proof
[(((triple1 ((triple1) -> rule4)) -> rule3))]
("Erin" "is" "big" "-")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Erin is not big.
("Erin" "is" "big" "-")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is big.
False
4
inv-proof
[(((triple1 ((triple1) -> rule4)) -> rule3))]
("Erin" "is" "big" "+")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Erin is not big.
("Erin" "is" "big" "-")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is cold.
True
7
proof
[(((((triple1) -> rule4) ((triple1 ((triple1) -> rule4)) -> rule3)) -> rule6))]
("Erin" "is" "cold" "+")
((((triple1) -> (rule4 % int3)) ((triple1 ((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is not big.
("Erin" "is" "big" "-")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is not cold.
False
7
inv-proof
[(((((triple1) -> rule4) ((triple1 ((triple1) -> rule4)) -> rule3)) -> rule6))]
("Erin" "is" "cold" "-")
((((triple1) -> (rule4 % int3)) ((triple1 ((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is not big.
("Erin" "is" "big" "-")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is not rough.
Unknown
inv-rconc
[@1: Erin is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "rough" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
@0: Erin is young.[(triple1)] @1: Erin is quiet.[(((triple1) -> rule4))] @2: Erin is not big.[(((triple1 ((triple1) -> rule4)) -> rule3))] @3: Erin is cold.[(((((triple1) -> rule4) ((triple1 ((triple1) -> rule4)) -> rule3)) -> rule6))]
Erin is young.
("Erin" "is" "young" "+")
triple1
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple1) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is not big.
("Erin" "is" "big" "-")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Erin is not big.
("Erin" "is" "big" "-")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
((((triple1) -> (rule4 % int3)) ((triple1 ((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is not big.
("Erin" "is" "big" "-")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3