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