Bob is blue. Bob is furry. Dave is cold. Dave is nice. Dave is not quiet. Dave is rough. Erin is not cold. Erin is not furry. Erin is green. Fiona is cold. Fiona is furry. Fiona is not nice. If someone is blue and green then they are rough. Quiet people are nice. All rough people are nice. If Dave is rough then Dave is nice. If Dave is cold then Dave is not quiet. If someone is green then they are blue. If someone is quiet then they are not blue. If Erin is not nice then Erin is furry.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is not quiet.
("Dave" "is" "quiet" "-")
Dave is rough.
("Dave" "is" "rough" "+")
Erin is not cold.
("Erin" "is" "cold" "-")
Erin is not furry.
("Erin" "is" "furry" "-")
Erin is green.
("Erin" "is" "green" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is not nice.
("Fiona" "is" "nice" "-")
If someone is blue and green then they are rough.
((("someone" "is" "blue" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
Quiet people are nice.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
All rough people are nice.
((("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
If Dave is rough then Dave is nice.
((("Dave" "is" "rough" "+")) -> ("Dave" "is" "nice" "+"))
If Dave is cold then Dave is not quiet.
((("Dave" "is" "cold" "+")) -> ("Dave" "is" "quiet" "-"))
If someone is green then they are blue.
((("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
If someone is quiet then they are not blue.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "blue" "-"))
If Erin is not nice then Erin is furry.
((("Erin" "is" "nice" "~")) -> ("Erin" "is" "furry" "+"))
Fiona is not nice.
True
1
proof
[(triple12)]
("Fiona" "is" "nice" "-")
triple12
Dave is not cold.
False
1
inv-proof
[(triple3)]
("Dave" "is" "cold" "-")
triple3
Erin is blue.
True
2
proof
[(((triple9) -> rule6))]
("Erin" "is" "blue" "+")
((triple9) -> (rule6 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is not blue.
False
2
inv-proof
[(((triple9) -> rule6))]
("Erin" "is" "blue" "-")
((triple9) -> (rule6 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Dave is not blue.
Unknown
inv-rconc
[@1: Dave is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "blue" "-")
Fiona is blue.
Unknown
rconc
[@1: Fiona is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "blue" "+")
Fiona is not quiet.
Unknown
inv-random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
@0: Bob is blue.[(triple1)] Bob is furry.[(triple2)] Dave is cold.[(triple3)] Dave is nice.[(triple4 OR ((triple6) -> rule3) OR ((triple6) -> rule4))] Dave is not quiet.[(triple5 OR ((triple3) -> rule5))] Dave is rough.[(triple6)] Erin is green.[(triple9)] Erin is not cold.[(triple7)] Erin is not furry.[(triple8)] Fiona is cold.[(triple10)] Fiona is furry.[(triple11)] Fiona is not nice.[(triple12)] @1: Erin is blue.[(((triple9) -> rule6))] @2: Erin is rough.[(((((triple9) -> rule6) triple9) -> rule1))] @3: Erin is nice.[(((((((triple9) -> rule6) triple9) -> rule1)) -> rule3))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Dave is cold.
("Dave" "is" "cold" "+")
triple3
Dave is nice.
("Dave" "is" "nice" "+")
triple4
((triple6) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((triple6) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is not quiet.
("Dave" "is" "quiet" "-")
triple5
((triple3) -> (rule5 % int1))
Dave is not quiet.
("Dave" "is" "quiet" "-")
int1
Dave is rough.
("Dave" "is" "rough" "+")
triple6
Erin is green.
("Erin" "is" "green" "+")
triple9
Erin is not cold.
("Erin" "is" "cold" "-")
triple7
Erin is not furry.
("Erin" "is" "furry" "-")
triple8
Fiona is cold.
("Fiona" "is" "cold" "+")
triple10
Fiona is furry.
("Fiona" "is" "furry" "+")
triple11
Fiona is not nice.
("Fiona" "is" "nice" "-")
triple12
Erin is blue.
("Erin" "is" "blue" "+")
((triple9) -> (rule6 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
((((triple9) -> (rule6 % int2)) triple9) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
((((((triple9) -> (rule6 % int3)) triple9) -> (rule1 % int2))) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3