Anne is blue. Anne is cold. Anne is nice. Anne is red. Anne is rough. Anne is round. Anne is smart. Dave is blue. Dave is cold. Dave is round. Erin is nice. Erin is red. Erin is round. Erin is smart. Fiona is blue. Fiona is cold. All cold people are rough. If Fiona is rough then Fiona is smart. If Anne is rough then Anne is smart. If someone is nice and not red then they are cold. Red people are round. If Erin is cold and Erin is not rough then Erin is round.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is round.
("Dave" "is" "round" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
All cold people are rough.
((("someone" "is" "cold" "+")) -> ("someone" "is" "rough" "+"))
If Fiona is rough then Fiona is smart.
((("Fiona" "is" "rough" "+")) -> ("Fiona" "is" "smart" "+"))
If Anne is rough then Anne is smart.
((("Anne" "is" "rough" "+")) -> ("Anne" "is" "smart" "+"))
If someone is nice and not red then they are cold.
((("someone" "is" "nice" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "cold" "+"))
Red people are round.
((("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
If Erin is cold and Erin is not rough then Erin is round.
((("Erin" "is" "cold" "+") ("Erin" "is" "rough" "~")) -> ("Erin" "is" "round" "+"))
Erin is round.
True
1
proof
[(triple13 OR ((triple12) -> rule5))]
("Erin" "is" "round" "+")
triple13
((triple12) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Dave is not cold.
False
1
inv-proof
[(triple9)]
("Dave" "is" "cold" "-")
triple9
Erin is not cold.
Unknown
inv-rconc
[@1: Erin is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "cold" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Anne is blue.[(triple1)] Anne is cold.[(triple2)] Anne is nice.[(triple3)] Anne is red.[(triple4)] Anne is rough.[(triple5 OR ((triple2) -> rule1))] Anne is round.[(triple6 OR ((triple4) -> rule5))] Anne is smart.[(triple7 OR ((triple5) -> rule3) OR ((((triple2) -> rule1)) -> rule3))] Dave is blue.[(triple8)] Dave is cold.[(triple9)] Dave is round.[(triple10)] Erin is nice.[(triple11)] Erin is red.[(triple12)] Erin is round.[(triple13 OR ((triple12) -> rule5))] Erin is smart.[(triple14)] Fiona is blue.[(triple15)] Fiona is cold.[(triple16)] @1: Dave is rough.[(((triple9) -> rule1))] Fiona is rough.[(((triple16) -> rule1))] @2: Fiona is smart.[(((((triple16) -> rule1)) -> rule2))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is nice.
("Anne" "is" "nice" "+")
triple3
Anne is red.
("Anne" "is" "red" "+")
triple4
Anne is rough.
("Anne" "is" "rough" "+")
triple5
((triple2) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
triple6
((triple4) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
triple7
((triple5) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
triple8
Dave is cold.
("Dave" "is" "cold" "+")
triple9
Dave is round.
("Dave" "is" "round" "+")
triple10
Erin is nice.
("Erin" "is" "nice" "+")
triple11
Erin is red.
("Erin" "is" "red" "+")
triple12
Erin is round.
("Erin" "is" "round" "+")
triple13
((triple12) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
triple14
Fiona is blue.
("Fiona" "is" "blue" "+")
triple15
Fiona is cold.
("Fiona" "is" "cold" "+")
triple16
Dave is rough.
("Dave" "is" "rough" "+")
((triple9) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
((triple16) -> (rule1 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
((((triple16) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2