Dave is green. Erin is blue. Gary is not white. Harry is big. If Dave is white and Dave is not furry then Dave is round. If Gary is round and Gary is not green then Gary is furry. Green things are white. If something is white then it is big. If Gary is white then Gary is big. Big, green things are blue. If something is big and not white then it is not smart. If something is white and green then it is smart.
Dave is green.
("Dave" "is" "green" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Gary is not white.
("Gary" "is" "white" "-")
Harry is big.
("Harry" "is" "big" "+")
If Dave is white and Dave is not furry then Dave is round.
((("Dave" "is" "white" "+") ("Dave" "is" "furry" "~")) -> ("Dave" "is" "round" "+"))
If Gary is round and Gary is not green then Gary is furry.
((("Gary" "is" "round" "+") ("Gary" "is" "green" "~")) -> ("Gary" "is" "furry" "+"))
Green things are white.
((("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
If something is white then it is big.
((("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
If Gary is white then Gary is big.
((("Gary" "is" "white" "+")) -> ("Gary" "is" "big" "+"))
Big, green things are blue.
((("something" "is" "big" "+") ("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
If something is big and not white then it is not smart.
((("something" "is" "big" "+") ("something" "is" "white" "~")) -> ("something" "is" "smart" "-"))
If something is white and green then it is smart.
((("something" "is" "white" "+") ("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
Harry is big.
True
1
proof
[(triple4)]
("Harry" "is" "big" "+")
triple4
Gary is white.
False
1
inv-proof
[(triple3)]
("Gary" "is" "white" "+")
triple3
Dave is white.
True
2
proof
[(((triple1) -> rule3))]
("Dave" "is" "white" "+")
((triple1) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is not white.
False
2
inv-proof
[(((triple1) -> rule3))]
("Dave" "is" "white" "-")
((triple1) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is smart.
True
4
proof
[(((((triple1) -> rule3) triple1) -> rule8))]
("Dave" "is" "smart" "+")
((((triple1) -> (rule3 % int2)) triple1) -> (rule8 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is not big.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule4))]
("Dave" "is" "big" "-")
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is blue.
True
5
proof
[(((((((triple1) -> rule3)) -> rule4) triple1) -> rule6))]
("Dave" "is" "blue" "+")
((((((triple1) -> (rule3 % int3))) -> (rule4 % int2)) triple1) -> (rule6 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is not blue.
False
5
inv-proof
[(((((((triple1) -> rule3)) -> rule4) triple1) -> rule6))]
("Dave" "is" "blue" "-")
((((((triple1) -> (rule3 % int3))) -> (rule4 % int2)) triple1) -> (rule6 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is not round.
Unknown
inv-rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "round" "-")
Erin is big.
Unknown
rconc
[@2: Erin is big.[CWA. Example of deepest failure = (rule4 <- rule3 <- FAIL)]]
("Erin" "is" "big" "+")
Gary is not smart.
Unknown
inv-rconc
[@1: Gary is smart.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Gary" "is" "smart" "-")
Gary is blue.
Unknown
rconc
[@1: Gary is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "blue" "+")
Erin is not green.
Unknown
inv-random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
@0: Dave is green.[(triple1)] Erin is blue.[(triple2)] Gary is not white.[(triple3)] Harry is big.[(triple4)] @1: Dave is white.[(((triple1) -> rule3))] @2: Dave is big.[(((((triple1) -> rule3)) -> rule4))] Dave is smart.[(((((triple1) -> rule3) triple1) -> rule8))] @3: Dave is blue.[(((((((triple1) -> rule3)) -> rule4) triple1) -> rule6))]
Dave is green.
("Dave" "is" "green" "+")
triple1
Erin is blue.
("Erin" "is" "blue" "+")
triple2
Gary is not white.
("Gary" "is" "white" "-")
triple3
Harry is big.
("Harry" "is" "big" "+")
triple4
Dave is white.
("Dave" "is" "white" "+")
((triple1) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
((((triple1) -> (rule3 % int2)) triple1) -> (rule8 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
((((((triple1) -> (rule3 % int3))) -> (rule4 % int2)) triple1) -> (rule6 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3