Erin is green. Erin is kind. Erin is rough. Erin is smart. Fiona is green. Fiona is smart. Gary is green. Gary is kind. Gary is nice. Gary is rough. Gary is round. Gary is smart. If Fiona is quiet then Fiona is nice. If Gary is round then Gary is quiet. If something is kind and round then it is rough.
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is smart.
("Gary" "is" "smart" "+")
If Fiona is quiet then Fiona is nice.
((("Fiona" "is" "quiet" "+")) -> ("Fiona" "is" "nice" "+"))
If Gary is round then Gary is quiet.
((("Gary" "is" "round" "+")) -> ("Gary" "is" "quiet" "+"))
If something is kind and round then it is rough.
((("something" "is" "kind" "+") ("something" "is" "round" "+")) -> ("something" "is" "rough" "+"))
Erin is smart.
True
1
proof
[(triple4)]
("Erin" "is" "smart" "+")
triple4
Gary is not nice.
False
1
inv-proof
[(triple9)]
("Gary" "is" "nice" "-")
triple9
Gary is quiet.
True
2
proof
[(((triple11) -> rule2))]
("Gary" "is" "quiet" "+")
((triple11) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is not quiet.
False
2
inv-proof
[(((triple11) -> rule2))]
("Gary" "is" "quiet" "-")
((triple11) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Fiona is not rough.
Unknown
inv-rconc
[@1: Fiona is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "rough" "-")
Fiona is nice.
Unknown
rconc
[@1: Fiona is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "nice" "+")
Fiona is not kind.
Unknown
inv-random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "-")
Fiona is round.
Unknown
random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "+")
@0: Erin is green.[(triple1)] Erin is kind.[(triple2)] Erin is rough.[(triple3)] Erin is smart.[(triple4)] Fiona is green.[(triple5)] Fiona is smart.[(triple6)] Gary is green.[(triple7)] Gary is kind.[(triple8)] Gary is nice.[(triple9)] Gary is rough.[(triple10 OR ((triple8 triple11) -> rule3))] Gary is round.[(triple11)] Gary is smart.[(triple12)] @1: Gary is quiet.[(((triple11) -> rule2))]
Erin is green.
("Erin" "is" "green" "+")
triple1
Erin is kind.
("Erin" "is" "kind" "+")
triple2
Erin is rough.
("Erin" "is" "rough" "+")
triple3
Erin is smart.
("Erin" "is" "smart" "+")
triple4
Fiona is green.
("Fiona" "is" "green" "+")
triple5
Fiona is smart.
("Fiona" "is" "smart" "+")
triple6
Gary is green.
("Gary" "is" "green" "+")
triple7
Gary is kind.
("Gary" "is" "kind" "+")
triple8
Gary is nice.
("Gary" "is" "nice" "+")
triple9
Gary is rough.
("Gary" "is" "rough" "+")
triple10
((triple8 triple11) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
triple11
Gary is smart.
("Gary" "is" "smart" "+")
triple12
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple11) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1