Charlie is big. Erin is round. Erin is smart. If someone is kind then they are big. All big, round people are green. If Erin is round then Erin is quiet.
Charlie is big.
("Charlie" "is" "big" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
If someone is kind then they are big.
((("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
All big, round people are green.
((("someone" "is" "big" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "green" "+"))
If Erin is round then Erin is quiet.
((("Erin" "is" "round" "+")) -> ("Erin" "is" "quiet" "+"))
Erin is smart.
True
1
proof
[(triple3)]
("Erin" "is" "smart" "+")
triple3
Charlie is not big.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "big" "-")
triple1
Erin is quiet.
True
2
proof
[(((triple2) -> rule3))]
("Erin" "is" "quiet" "+")
((triple2) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is not quiet.
False
2
inv-proof
[(((triple2) -> rule3))]
("Erin" "is" "quiet" "-")
((triple2) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is not green.
Unknown
inv-rconc
[@2: Erin is green.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Erin" "is" "green" "-")
Charlie is green.
Unknown
rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "green" "+")
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Erin is cold.
Unknown
random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "+")
@0: Charlie is big.[(triple1)] Erin is round.[(triple2)] Erin is smart.[(triple3)] @1: Erin is quiet.[(((triple2) -> rule3))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Erin is round.
("Erin" "is" "round" "+")
triple2
Erin is smart.
("Erin" "is" "smart" "+")
triple3
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple2) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1