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