Charlie is nice. Dave is not big. Erin is nice. Erin is rough. Erin is smart. Erin is white. Gary is big. Rough things are smart. If something is white and not cold then it is not smart. Big things are not smart. If Erin is white and Erin is cold then Erin is nice. If something is smart then it is white. If something is blue then it is nice.
Charlie is nice.
("Charlie" "is" "nice" "+")
Dave is not big.
("Dave" "is" "big" "-")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Gary is big.
("Gary" "is" "big" "+")
Rough things are smart.
((("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
If something is white and not cold then it is not smart.
((("something" "is" "white" "+") ("something" "is" "cold" "~")) -> ("something" "is" "smart" "-"))
Big things are not smart.
((("something" "is" "big" "+")) -> ("something" "is" "smart" "-"))
If Erin is white and Erin is cold then Erin is nice.
((("Erin" "is" "white" "+") ("Erin" "is" "cold" "+")) -> ("Erin" "is" "nice" "+"))
If something is smart then it is white.
((("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
If something is blue then it is nice.
((("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
Erin is smart.
True
1
proof
[(triple5 OR ((triple4) -> rule1))]
("Erin" "is" "smart" "+")
triple5
((triple4) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Gary is not big.
False
1
inv-proof
[(triple7)]
("Gary" "is" "big" "-")
triple7
Charlie is not smart.
Unknown
inv-rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "smart" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
@0: Charlie is nice.[(triple1)] Dave is not big.[(triple2)] Erin is nice.[(triple3)] Erin is rough.[(triple4)] Erin is smart.[(triple5 OR ((triple4) -> rule1))] Erin is white.[(triple6 OR ((triple5) -> rule5) OR ((((triple4) -> rule1)) -> rule5))] Gary is big.[(triple7)] @1: Gary is not smart.[(((triple7) -> rule3))]
Charlie is nice.
("Charlie" "is" "nice" "+")
triple1
Dave is not big.
("Dave" "is" "big" "-")
triple2
Erin is nice.
("Erin" "is" "nice" "+")
triple3
Erin is rough.
("Erin" "is" "rough" "+")
triple4
Erin is smart.
("Erin" "is" "smart" "+")
triple5
((triple4) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
triple6
((triple5) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
triple7
Gary is not smart.
("Gary" "is" "smart" "-")
((triple7) -> (rule3 % int1))
Gary is not smart.
("Gary" "is" "smart" "-")
int1