Anne is red. Bob is nice. Fiona is furry. Gary is blue. If Gary is red and Gary is not furry then Gary is nice. If something is smart and not big then it is nice. If something is red then it is nice. If something is smart and furry then it is round. All smart things are blue. If something is big then it is red. If something is furry then it is red. If something is nice then it is smart.
Anne is red.
("Anne" "is" "red" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Gary is blue.
("Gary" "is" "blue" "+")
If Gary is red and Gary is not furry then Gary is nice.
((("Gary" "is" "red" "+") ("Gary" "is" "furry" "~")) -> ("Gary" "is" "nice" "+"))
If something is smart and not big then it is nice.
((("something" "is" "smart" "+") ("something" "is" "big" "~")) -> ("something" "is" "nice" "+"))
If something is red then it is nice.
((("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
If something is smart and furry then it is round.
((("something" "is" "smart" "+") ("something" "is" "furry" "+")) -> ("something" "is" "round" "+"))
All smart things are blue.
((("something" "is" "smart" "+")) -> ("something" "is" "blue" "+"))
If something is big then it is red.
((("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
If something is furry then it is red.
((("something" "is" "furry" "+")) -> ("something" "is" "red" "+"))
If something is nice then it is smart.
((("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
Anne is red.
True
1
proof
[(triple1)]
("Anne" "is" "red" "+")
triple1
Fiona is not furry.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "furry" "-")
triple3
Bob is smart.
True
2
proof
[(((triple2) -> rule8))]
("Bob" "is" "smart" "+")
((triple2) -> (rule8 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Fiona is not red.
False
2
inv-proof
[(((triple3) -> rule7))]
("Fiona" "is" "red" "-")
((triple3) -> (rule7 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Bob is blue.
True
3
proof
[(((((triple2) -> rule8)) -> rule5))]
("Bob" "is" "blue" "+")
((((triple2) -> (rule8 % int2))) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is not blue.
False
3
inv-proof
[(((((triple2) -> rule8)) -> rule5))]
("Bob" "is" "blue" "-")
((((triple2) -> (rule8 % int2))) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Anne is blue.
True
4
proof
[(((((((triple1) -> rule3)) -> rule8)) -> rule5))]
("Anne" "is" "blue" "+")
((((((triple1) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Fiona is not smart.
False
4
inv-proof
[(((((((triple3) -> rule7)) -> rule3)) -> rule8))]
("Fiona" "is" "smart" "-")
((((((triple3) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Bob is not round.
Unknown
inv-rconc
[@1: Bob is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "round" "-")
Bob is red.
Unknown
rconc
[@1: Bob is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "red" "+")
Gary is not red.
Unknown
inv-rconc
[@1: Gary is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "red" "-")
Gary is nice.
Unknown
rconc
[@2: Gary is nice.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("Gary" "is" "nice" "+")
Anne is not big.
Unknown
inv-random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "-")
Fiona is big.
Unknown
random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "+")
Gary is not big.
Unknown
inv-random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
@0: Anne is red.[(triple1)] Bob is nice.[(triple2)] Fiona is furry.[(triple3)] Gary is blue.[(triple4)] @1: Anne is nice.[(((triple1) -> rule3))] Bob is smart.[(((triple2) -> rule8))] Fiona is red.[(((triple3) -> rule7))] @2: Anne is smart.[(((((triple1) -> rule3)) -> rule8))] Bob is blue.[(((((triple2) -> rule8)) -> rule5))] Fiona is nice.[(((((triple3) -> rule7)) -> rule3))] @3: Anne is blue.[(((((((triple1) -> rule3)) -> rule8)) -> rule5))] Fiona is smart.[(((((((triple3) -> rule7)) -> rule3)) -> rule8))] @4: Fiona is blue.[(((((((((triple3) -> rule7)) -> rule3)) -> rule8)) -> rule5))] Fiona is round.[(((((((((triple3) -> rule7)) -> rule3)) -> rule8) triple3) -> rule4))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Fiona is furry.
("Fiona" "is" "furry" "+")
triple3
Gary is blue.
("Gary" "is" "blue" "+")
triple4
Anne is nice.
("Anne" "is" "nice" "+")
((triple1) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((triple2) -> (rule8 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
((triple3) -> (rule7 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
((((triple1) -> (rule3 % int2))) -> (rule8 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
((((triple2) -> (rule8 % int2))) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
((((triple3) -> (rule7 % int2))) -> (rule3 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
((((((triple1) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
((((((triple3) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Fiona is blue.
("Fiona" "is" "blue" "+")
((((((((triple3) -> (rule7 % int4))) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
int4
Fiona is round.
("Fiona" "is" "round" "+")
((((((((triple3) -> (rule7 % int4))) -> (rule3 % int3))) -> (rule8 % int2)) triple3) -> (rule4 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
int4