Charlie is blue. Charlie is green. Charlie is kind. Charlie is red. Erin is big. Erin is not red. Erin is round. If something is blue then it is rough. Big things are not rough. If something is red then it is rough. If something is red and blue then it is not big. Round, rough things are big. If Erin is red and Erin is not round then Erin is green. All big, red things are blue. If something is red and not rough then it is kind.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is not red.
("Erin" "is" "red" "-")
Erin is round.
("Erin" "is" "round" "+")
If something is blue then it is rough.
((("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
Big things are not rough.
((("something" "is" "big" "+")) -> ("something" "is" "rough" "-"))
If something is red then it is rough.
((("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
If something is red and blue then it is not big.
((("something" "is" "red" "+") ("something" "is" "blue" "+")) -> ("something" "is" "big" "-"))
Round, rough things are big.
((("something" "is" "round" "+") ("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
If Erin is red and Erin is not round then Erin is green.
((("Erin" "is" "red" "+") ("Erin" "is" "round" "~")) -> ("Erin" "is" "green" "+"))
All big, red things are blue.
((("something" "is" "big" "+") ("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
If something is red and not rough then it is kind.
((("something" "is" "red" "+") ("something" "is" "rough" "~")) -> ("something" "is" "kind" "+"))
Charlie is kind.
True
1
proof
[(triple3)]
("Charlie" "is" "kind" "+")
triple3
Erin is not round.
False
1
inv-proof
[(triple7)]
("Erin" "is" "round" "-")
triple7
Charlie is rough.
True
2
proof
[(((triple1) -> rule1) OR ((triple4) -> rule3))]
("Charlie" "is" "rough" "+")
((triple1) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((triple4) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is big.
False
3
inv-proof
[(((triple4 triple1) -> rule4))]
("Charlie" "is" "big" "+")
((triple4 triple1) -> (rule4 % int1))
Charlie is not big.
("Charlie" "is" "big" "-")
int1
Erin is not kind.
Unknown
inv-rconc
[@1: Erin is kind.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Erin" "is" "kind" "-")
Erin is green.
Unknown
rconc
[@1: Erin is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "green" "+")
@0: Charlie is blue.[(triple1)] Charlie is green.[(triple2)] Charlie is kind.[(triple3)] Charlie is red.[(triple4)] Erin is big.[(triple5)] Erin is not red.[(triple6)] Erin is round.[(triple7)] @1: Charlie is not big.[(((triple4 triple1) -> rule4))] Charlie is rough.[(((triple1) -> rule1) OR ((triple4) -> rule3))] Erin is not rough.[(((triple5) -> rule2))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Charlie is red.
("Charlie" "is" "red" "+")
triple4
Erin is big.
("Erin" "is" "big" "+")
triple5
Erin is not red.
("Erin" "is" "red" "-")
triple6
Erin is round.
("Erin" "is" "round" "+")
triple7
Charlie is not big.
("Charlie" "is" "big" "-")
((triple4 triple1) -> (rule4 % int1))
Charlie is not big.
("Charlie" "is" "big" "-")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple1) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((triple4) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Erin is not rough.
("Erin" "is" "rough" "-")
((triple5) -> (rule2 % int1))
Erin is not rough.
("Erin" "is" "rough" "-")
int1