Anne is green. Anne is red. Anne is round. Anne is smart. Anne is white. Dave is blue. Dave is cold. Dave is green. Dave is red. Dave is round. Dave is smart. Dave is white. Erin is blue. Erin is cold. Erin is green. Erin is white. All green, cold things are smart. Smart things are red. Cold things are blue.
Anne is green.
("Anne" "is" "green" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is white.
("Anne" "is" "white" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is white.
("Erin" "is" "white" "+")
All green, cold things are smart.
((("something" "is" "green" "+") ("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
Smart things are red.
((("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
Cold things are blue.
((("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
Dave is cold.
True
1
proof
[(triple7)]
("Dave" "is" "cold" "+")
triple7
Anne is not green.
False
1
inv-proof
[(triple1)]
("Anne" "is" "green" "-")
triple1
Erin is smart.
True
3
proof
[(((triple15 triple14) -> rule1))]
("Erin" "is" "smart" "+")
((triple15 triple14) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is not smart.
False
3
inv-proof
[(((triple15 triple14) -> rule1))]
("Erin" "is" "smart" "-")
((triple15 triple14) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is red.
True
4
proof
[(((((triple15 triple14) -> rule1)) -> rule2))]
("Erin" "is" "red" "+")
((((triple15 triple14) -> (rule1 % int2))) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is not red.
False
4
inv-proof
[(((((triple15 triple14) -> rule1)) -> rule2))]
("Erin" "is" "red" "-")
((((triple15 triple14) -> (rule1 % int2))) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Anne is not blue.
Unknown
inv-rconc
[@1: Anne is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "blue" "-")
Anne is cold.
Unknown
random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "+")
@0: Anne is green.[(triple1)] Anne is red.[(triple2 OR ((triple4) -> rule2))] Anne is round.[(triple3)] Anne is smart.[(triple4)] Anne is white.[(triple5)] Dave is blue.[(triple6 OR ((triple7) -> rule3))] Dave is cold.[(triple7)] Dave is green.[(triple8)] Dave is red.[(triple9 OR ((triple11) -> rule2) OR ((((triple8 triple7) -> rule1)) -> rule2))] Dave is round.[(triple10)] Dave is smart.[(triple11 OR ((triple8 triple7) -> rule1))] Dave is white.[(triple12)] Erin is blue.[(triple13 OR ((triple14) -> rule3))] Erin is cold.[(triple14)] Erin is green.[(triple15)] Erin is white.[(triple16)] @1: Erin is smart.[(((triple15 triple14) -> rule1))] @2: Erin is red.[(((((triple15 triple14) -> rule1)) -> rule2))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
((triple4) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
triple3
Anne is smart.
("Anne" "is" "smart" "+")
triple4
Anne is white.
("Anne" "is" "white" "+")
triple5
Dave is blue.
("Dave" "is" "blue" "+")
triple6
((triple7) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
triple7
Dave is green.
("Dave" "is" "green" "+")
triple8
Dave is red.
("Dave" "is" "red" "+")
triple9
((triple11) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((((triple8 triple7) -> (rule1 % int2))) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
triple10
Dave is smart.
("Dave" "is" "smart" "+")
triple11
((triple8 triple7) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
triple12
Erin is blue.
("Erin" "is" "blue" "+")
triple13
((triple14) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
triple14
Erin is green.
("Erin" "is" "green" "+")
triple15
Erin is white.
("Erin" "is" "white" "+")
triple16
Erin is smart.
("Erin" "is" "smart" "+")
((triple15 triple14) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
((((triple15 triple14) -> (rule1 % int2))) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2