Bob is smart. Dave is nice. Erin is big. Erin is nice. Erin is quiet. Erin is round. Fiona is rough. If something is round then it is white. If something is quiet and round then it is big. If Dave is smart and Dave is round then Dave is nice.
Bob is smart.
("Bob" "is" "smart" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is round.
("Erin" "is" "round" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
If something is round then it is white.
((("something" "is" "round" "+")) -> ("something" "is" "white" "+"))
If something is quiet and round then it is big.
((("something" "is" "quiet" "+") ("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
If Dave is smart and Dave is round then Dave is nice.
((("Dave" "is" "smart" "+") ("Dave" "is" "round" "+")) -> ("Dave" "is" "nice" "+"))
Erin is big.
True
1
proof
[(triple3 OR ((triple5 triple6) -> rule2))]
("Erin" "is" "big" "+")
triple3
((triple5 triple6) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Fiona is not rough.
False
1
inv-proof
[(triple7)]
("Fiona" "is" "rough" "-")
triple7
Dave is not big.
Unknown
inv-rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "big" "-")
Erin is smart.
Unknown
random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "+")
@0: Bob is smart.[(triple1)] Dave is nice.[(triple2)] Erin is big.[(triple3 OR ((triple5 triple6) -> rule2))] Erin is nice.[(triple4)] Erin is quiet.[(triple5)] Erin is round.[(triple6)] Fiona is rough.[(triple7)] @1: Erin is white.[(((triple6) -> rule1))]
Bob is smart.
("Bob" "is" "smart" "+")
triple1
Dave is nice.
("Dave" "is" "nice" "+")
triple2
Erin is big.
("Erin" "is" "big" "+")
triple3
((triple5 triple6) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
triple4
Erin is quiet.
("Erin" "is" "quiet" "+")
triple5
Erin is round.
("Erin" "is" "round" "+")
triple6
Fiona is rough.
("Fiona" "is" "rough" "+")
triple7
Erin is white.
("Erin" "is" "white" "+")
((triple6) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1