Charlie is big. Erin is not cold. Erin is green. Green things are quiet. If something is big and not quiet then it is young. If Erin is young and Erin is quiet then Erin is not big. If something is big and not quiet then it is kind. If something is quiet and green then it is not kind. All cold, big things are not white. If something is green then it is white. If something is big and not young then it is not cold.
Charlie is big.
("Charlie" "is" "big" "+")
Erin is not cold.
("Erin" "is" "cold" "-")
Erin is green.
("Erin" "is" "green" "+")
Green things are quiet.
((("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
If something is big and not quiet then it is young.
((("something" "is" "big" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "young" "+"))
If Erin is young and Erin is quiet then Erin is not big.
((("Erin" "is" "young" "+") ("Erin" "is" "quiet" "+")) -> ("Erin" "is" "big" "-"))
If something is big and not quiet then it is kind.
((("something" "is" "big" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "kind" "+"))
If something is quiet and green then it is not kind.
((("something" "is" "quiet" "+") ("something" "is" "green" "+")) -> ("something" "is" "kind" "-"))
All cold, big things are not white.
((("something" "is" "cold" "+") ("something" "is" "big" "+")) -> ("something" "is" "white" "-"))
If something is green then it is white.
((("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
If something is big and not young then it is not cold.
((("something" "is" "big" "+") ("something" "is" "young" "~")) -> ("something" "is" "cold" "-"))
Erin is not cold.
True
1
proof
[(triple2)]
("Erin" "is" "cold" "-")
triple2
Erin is cold.
False
1
inv-proof
[(triple2)]
("Erin" "is" "cold" "+")
triple2
Erin is quiet.
True
2
proof
[(((triple3) -> rule1))]
("Erin" "is" "quiet" "+")
((triple3) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is not white.
False
2
inv-proof
[(((triple3) -> rule7))]
("Erin" "is" "white" "-")
((triple3) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is not kind.
True
4
proof
[(((((triple3) -> rule1) triple3) -> rule5))]
("Erin" "is" "kind" "-")
((((triple3) -> (rule1 % int2)) triple3) -> (rule5 % int1))
Erin is not kind.
("Erin" "is" "kind" "-")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is kind.
False
4
inv-proof
[(((((triple3) -> rule1) triple3) -> rule5))]
("Erin" "is" "kind" "+")
((((triple3) -> (rule1 % int2)) triple3) -> (rule5 % int1))
Erin is not kind.
("Erin" "is" "kind" "-")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Charlie is not young.
Unknown
inv-rconc
[@1: Charlie is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "young" "-")
Charlie is white.
Unknown
rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Charlie" "is" "white" "+")
Charlie is not quiet.
Unknown
inv-rconc
[@1: Charlie is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "quiet" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
Charlie is not green.
Unknown
inv-random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
@0: Charlie is big.[(triple1)] Erin is green.[(triple3)] Erin is not cold.[(triple2)] @1: Erin is quiet.[(((triple3) -> rule1))] Erin is white.[(((triple3) -> rule7))] @2: Erin is not kind.[(((((triple3) -> rule1) triple3) -> rule5))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Erin is green.
("Erin" "is" "green" "+")
triple3
Erin is not cold.
("Erin" "is" "cold" "-")
triple2
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple3) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((triple3) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is not kind.
("Erin" "is" "kind" "-")
((((triple3) -> (rule1 % int2)) triple3) -> (rule5 % int1))
Erin is not kind.
("Erin" "is" "kind" "-")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2