Charlie is not quiet. Erin is big. Fiona is green. Gary is quiet. Nice things are smart. Green things are big. If Erin is not kind then Erin is quiet.
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
Erin is big.
("Erin" "is" "big" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Nice things are smart.
((("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
Green things are big.
((("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
If Erin is not kind then Erin is quiet.
((("Erin" "is" "kind" "~")) -> ("Erin" "is" "quiet" "+"))
Erin is big.
True
1
proof
[(triple2)]
("Erin" "is" "big" "+")
triple2
Charlie is quiet.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "quiet" "+")
triple1
Fiona is big.
True
2
proof
[(((triple3) -> rule2))]
("Fiona" "is" "big" "+")
((triple3) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is not big.
False
2
inv-proof
[(((triple3) -> rule2))]
("Fiona" "is" "big" "-")
((triple3) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Charlie is not smart.
Unknown
inv-rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "smart" "-")
Gary is smart.
Unknown
rconc
[@1: Gary is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "smart" "+")
Gary is not nice.
Unknown
inv-random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "-")
Erin is cold.
Unknown
random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "+")
@0: Charlie is not quiet.[(triple1)] Erin is big.[(triple2)] Fiona is green.[(triple3)] Gary is quiet.[(triple4)] @1: Fiona is big.[(((triple3) -> rule2))]
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
triple1
Erin is big.
("Erin" "is" "big" "+")
triple2
Fiona is green.
("Fiona" "is" "green" "+")
triple3
Gary is quiet.
("Gary" "is" "quiet" "+")
triple4
Fiona is big.
("Fiona" "is" "big" "+")
((triple3) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1