Bob is blue. Bob is not furry. Bob is quiet. Dave is cold. Dave is not furry. Dave is kind. Dave is red. Fiona is not big. Fiona is kind. Fiona is quiet. Furry people are quiet. If someone is furry and not blue then they are cold. All quiet, blue people are cold. All cold people are red. If Fiona is cold then Fiona is red. If someone is blue and cold then they are big. If someone is kind and not cold then they are not big. If someone is big then they are kind.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is not furry.
("Bob" "is" "furry" "-")
Bob is quiet.
("Bob" "is" "quiet" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is not furry.
("Dave" "is" "furry" "-")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is red.
("Dave" "is" "red" "+")
Fiona is not big.
("Fiona" "is" "big" "-")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Furry people are quiet.
((("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
If someone is furry and not blue then they are cold.
((("someone" "is" "furry" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "cold" "+"))
All quiet, blue people are cold.
((("someone" "is" "quiet" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
All cold people are red.
((("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
If Fiona is cold then Fiona is red.
((("Fiona" "is" "cold" "+")) -> ("Fiona" "is" "red" "+"))
If someone is blue and cold then they are big.
((("someone" "is" "blue" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
If someone is kind and not cold then they are not big.
((("someone" "is" "kind" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "big" "-"))
If someone is big then they are kind.
((("someone" "is" "big" "+")) -> ("someone" "is" "kind" "+"))
Bob is blue.
True
1
proof
[(triple1)]
("Bob" "is" "blue" "+")
triple1
Bob is furry.
False
1
inv-proof
[(triple2)]
("Bob" "is" "furry" "+")
triple2
Bob is cold.
True
3
proof
[(((triple3 triple1) -> rule3))]
("Bob" "is" "cold" "+")
((triple3 triple1) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is not cold.
False
3
inv-proof
[(((triple3 triple1) -> rule3))]
("Bob" "is" "cold" "-")
((triple3 triple1) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is red.
True
4
proof
[(((((triple3 triple1) -> rule3)) -> rule4))]
("Bob" "is" "red" "+")
((((triple3 triple1) -> (rule3 % int2))) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is not red.
False
4
inv-proof
[(((((triple3 triple1) -> rule3)) -> rule4))]
("Bob" "is" "red" "-")
((((triple3 triple1) -> (rule3 % int2))) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is kind.
True
6
proof
[(((((triple1 ((triple3 triple1) -> rule3)) -> rule6)) -> rule8))]
("Bob" "is" "kind" "+")
((((triple1 ((triple3 triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is not kind.
False
6
inv-proof
[(((((triple1 ((triple3 triple1) -> rule3)) -> rule6)) -> rule8))]
("Bob" "is" "kind" "-")
((((triple1 ((triple3 triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Fiona is not red.
Unknown
inv-rconc
[@2: Fiona is red.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("Fiona" "is" "red" "-")
Dave is quiet.
Unknown
rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "quiet" "+")
Fiona is not cold.
Unknown
inv-rconc
[@1: Fiona is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "cold" "-")
Dave is big.
Unknown
rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "big" "+")
Fiona is not blue.
Unknown
inv-random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
@0: Bob is blue.[(triple1)] Bob is not furry.[(triple2)] Bob is quiet.[(triple3)] Dave is cold.[(triple4)] Dave is kind.[(triple6)] Dave is not furry.[(triple5)] Dave is red.[(triple7 OR ((triple4) -> rule4))] Fiona is kind.[(triple9)] Fiona is not big.[(triple8)] Fiona is quiet.[(triple10)] @1: Bob is cold.[(((triple3 triple1) -> rule3))] @2: Bob is big.[(((triple1 ((triple3 triple1) -> rule3)) -> rule6))] Bob is red.[(((((triple3 triple1) -> rule3)) -> rule4))] @3: Bob is kind.[(((((triple1 ((triple3 triple1) -> rule3)) -> rule6)) -> rule8))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is not furry.
("Bob" "is" "furry" "-")
triple2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
Dave is cold.
("Dave" "is" "cold" "+")
triple4
Dave is kind.
("Dave" "is" "kind" "+")
triple6
Dave is not furry.
("Dave" "is" "furry" "-")
triple5
Dave is red.
("Dave" "is" "red" "+")
triple7
((triple4) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
triple9
Fiona is not big.
("Fiona" "is" "big" "-")
triple8
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple10
Bob is cold.
("Bob" "is" "cold" "+")
((triple3 triple1) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
((triple1 ((triple3 triple1) -> (rule3 % int2))) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
((((triple3 triple1) -> (rule3 % int2))) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
((((triple1 ((triple3 triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3