Bob is not blue. Bob is not quiet. Bob is rough. Erin is green. Erin is nice. Erin is not quiet. Erin is smart. If something is blue and green then it is not rough. If something is green and nice then it is smart. Quiet, big things are not nice. All big things are nice. All blue, rough things are nice. If something is green then it is blue.
Bob is not blue.
("Bob" "is" "blue" "-")
Bob is not quiet.
("Bob" "is" "quiet" "-")
Bob is rough.
("Bob" "is" "rough" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is not quiet.
("Erin" "is" "quiet" "-")
Erin is smart.
("Erin" "is" "smart" "+")
If something is blue and green then it is not rough.
((("something" "is" "blue" "+") ("something" "is" "green" "+")) -> ("something" "is" "rough" "-"))
If something is green and nice then it is smart.
((("something" "is" "green" "+") ("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
Quiet, big things are not nice.
((("something" "is" "quiet" "+") ("something" "is" "big" "+")) -> ("something" "is" "nice" "-"))
All big things are nice.
((("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
All blue, rough things are nice.
((("something" "is" "blue" "+") ("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
If something is green then it is blue.
((("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
Bob is not blue.
True
1
proof
[(triple1)]
("Bob" "is" "blue" "-")
triple1
Bob is quiet.
False
1
inv-proof
[(triple2)]
("Bob" "is" "quiet" "+")
triple2
Erin is blue.
True
2
proof
[(((triple4) -> rule6))]
("Erin" "is" "blue" "+")
((triple4) -> (rule6 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is not blue.
False
2
inv-proof
[(((triple4) -> rule6))]
("Erin" "is" "blue" "-")
((triple4) -> (rule6 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is not rough.
True
4
proof
[(((((triple4) -> rule6) triple4) -> rule1))]
("Erin" "is" "rough" "-")
((((triple4) -> (rule6 % int2)) triple4) -> (rule1 % int1))
Erin is not rough.
("Erin" "is" "rough" "-")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is rough.
False
4
inv-proof
[(((((triple4) -> rule6) triple4) -> rule1))]
("Erin" "is" "rough" "+")
((((triple4) -> (rule6 % int2)) triple4) -> (rule1 % int1))
Erin is not rough.
("Erin" "is" "rough" "-")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Bob is not smart.
Unknown
inv-rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "smart" "-")
Bob is nice.
Unknown
rconc
[@1: Bob is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "nice" "+")
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
@0: Bob is not blue.[(triple1)] Bob is not quiet.[(triple2)] Bob is rough.[(triple3)] Erin is green.[(triple4)] Erin is nice.[(triple5)] Erin is not quiet.[(triple6)] Erin is smart.[(triple7 OR ((triple4 triple5) -> rule2))] @1: Erin is blue.[(((triple4) -> rule6))] @2: Erin is not rough.[(((((triple4) -> rule6) triple4) -> rule1))]
Bob is not blue.
("Bob" "is" "blue" "-")
triple1
Bob is not quiet.
("Bob" "is" "quiet" "-")
triple2
Bob is rough.
("Bob" "is" "rough" "+")
triple3
Erin is green.
("Erin" "is" "green" "+")
triple4
Erin is nice.
("Erin" "is" "nice" "+")
triple5
Erin is not quiet.
("Erin" "is" "quiet" "-")
triple6
Erin is smart.
("Erin" "is" "smart" "+")
triple7
((triple4 triple5) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((triple4) -> (rule6 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is not rough.
("Erin" "is" "rough" "-")
((((triple4) -> (rule6 % int2)) triple4) -> (rule1 % int1))
Erin is not rough.
("Erin" "is" "rough" "-")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2