Anne is not big. Dave is green. Dave is red. Dave is white. Erin is not furry. Erin is green. Erin is smart. Erin is white. Gary is furry. Gary is green. Gary is red. Gary is smart. All big things are white. If Gary is smart and Gary is white then Gary is blue. If Dave is red then Dave is green. Blue things are smart. Red, green things are blue. All smart, furry things are blue. Furry, white things are blue. If Anne is smart then Anne is red.
Anne is not big.
("Anne" "is" "big" "-")
Dave is green.
("Dave" "is" "green" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is not furry.
("Erin" "is" "furry" "-")
Erin is green.
("Erin" "is" "green" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is smart.
("Gary" "is" "smart" "+")
All big things are white.
((("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
If Gary is smart and Gary is white then Gary is blue.
((("Gary" "is" "smart" "+") ("Gary" "is" "white" "+")) -> ("Gary" "is" "blue" "+"))
If Dave is red then Dave is green.
((("Dave" "is" "red" "+")) -> ("Dave" "is" "green" "+"))
Blue things are smart.
((("something" "is" "blue" "+")) -> ("something" "is" "smart" "+"))
Red, green things are blue.
((("something" "is" "red" "+") ("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
All smart, furry things are blue.
((("something" "is" "smart" "+") ("something" "is" "furry" "+")) -> ("something" "is" "blue" "+"))
Furry, white things are blue.
((("something" "is" "furry" "+") ("something" "is" "white" "+")) -> ("something" "is" "blue" "+"))
If Anne is smart then Anne is red.
((("Anne" "is" "smart" "+")) -> ("Anne" "is" "red" "+"))
Dave is green.
True
1
proof
[(triple2 OR ((triple3) -> rule3))]
("Dave" "is" "green" "+")
triple2
((triple3) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Gary is not smart.
False
1
inv-proof
[(triple12 OR ((((triple11 triple10) -> rule5)) -> rule4))]
("Gary" "is" "smart" "-")
triple12
((((triple11 triple10) -> (rule5 % int2))) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is blue.
True
3
proof
[(((triple11 triple10) -> rule5) OR ((triple12 triple9) -> rule6))]
("Gary" "is" "blue" "+")
((triple11 triple10) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((triple12 triple9) -> (rule6 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Dave is not blue.
False
3
inv-proof
[(((triple3 triple2) -> rule5) OR ((triple3 ((triple3) -> rule3)) -> rule5))]
("Dave" "is" "blue" "-")
((triple3 triple2) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((triple3 ((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is smart.
True
4
proof
[(((((triple3 triple2) -> rule5)) -> rule4) OR ((((triple3 ((triple3) -> rule3)) -> rule5)) -> rule4))]
("Dave" "is" "smart" "+")
((((triple3 triple2) -> (rule5 % int2))) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
((((triple3 ((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is not smart.
False
4
inv-proof
[(((((triple3 triple2) -> rule5)) -> rule4) OR ((((triple3 ((triple3) -> rule3)) -> rule5)) -> rule4))]
("Dave" "is" "smart" "-")
((((triple3 triple2) -> (rule5 % int2))) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
((((triple3 ((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Erin is not blue.
Unknown
inv-rconc
[@1: Erin is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "blue" "-")
Anne is smart.
Unknown
rconc
[@2: Anne is smart.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("Anne" "is" "smart" "+")
Anne is not red.
Unknown
inv-rconc
[@3: Anne is red.[CWA. Example of deepest failure = (rule8 <- rule4 <- rule5 <- FAIL)]]
("Anne" "is" "red" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
Erin is not big.
Unknown
inv-random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
@0: Anne is not big.[(triple1)] Dave is green.[(triple2 OR ((triple3) -> rule3))] Dave is red.[(triple3)] Dave is white.[(triple4)] Erin is green.[(triple6)] Erin is not furry.[(triple5)] Erin is smart.[(triple7)] Erin is white.[(triple8)] Gary is furry.[(triple9)] Gary is green.[(triple10)] Gary is red.[(triple11)] Gary is smart.[(triple12 OR ((((triple11 triple10) -> rule5)) -> rule4))] @1: Dave is blue.[(((triple3 triple2) -> rule5) OR ((triple3 ((triple3) -> rule3)) -> rule5))] Gary is blue.[(((triple11 triple10) -> rule5) OR ((triple12 triple9) -> rule6))] @2: Dave is smart.[(((((triple3 triple2) -> rule5)) -> rule4) OR ((((triple3 ((triple3) -> rule3)) -> rule5)) -> rule4))]
Anne is not big.
("Anne" "is" "big" "-")
triple1
Dave is green.
("Dave" "is" "green" "+")
triple2
((triple3) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
triple3
Dave is white.
("Dave" "is" "white" "+")
triple4
Erin is green.
("Erin" "is" "green" "+")
triple6
Erin is not furry.
("Erin" "is" "furry" "-")
triple5
Erin is smart.
("Erin" "is" "smart" "+")
triple7
Erin is white.
("Erin" "is" "white" "+")
triple8
Gary is furry.
("Gary" "is" "furry" "+")
triple9
Gary is green.
("Gary" "is" "green" "+")
triple10
Gary is red.
("Gary" "is" "red" "+")
triple11
Gary is smart.
("Gary" "is" "smart" "+")
triple12
((((triple11 triple10) -> (rule5 % int2))) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
((triple3 triple2) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((triple3 ((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
((triple11 triple10) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((triple12 triple9) -> (rule6 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((((triple3 triple2) -> (rule5 % int2))) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
((((triple3 ((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3