Bob is round. Fiona is big. Gary is big. All round things are red. Furry things are cold. If something is round then it is red. All big, red things are cold. All round, red things are furry. Big, furry things are nice.
Bob is round.
("Bob" "is" "round" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Gary is big.
("Gary" "is" "big" "+")
All round things are red.
((("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
Furry things are cold.
((("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
If something is round then it is red.
((("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
All big, red things are cold.
((("something" "is" "big" "+") ("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
All round, red things are furry.
((("something" "is" "round" "+") ("something" "is" "red" "+")) -> ("something" "is" "furry" "+"))
Big, furry things are nice.
((("something" "is" "big" "+") ("something" "is" "furry" "+")) -> ("something" "is" "nice" "+"))
Fiona is big.
True
1
proof
[(triple2)]
("Fiona" "is" "big" "+")
triple2
Fiona is not big.
False
1
inv-proof
[(triple2)]
("Fiona" "is" "big" "-")
triple2
Bob is red.
True
2
proof
[(((triple1) -> rule1) OR ((triple1) -> rule3))]
("Bob" "is" "red" "+")
((triple1) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((triple1) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is not red.
False
2
inv-proof
[(((triple1) -> rule1) OR ((triple1) -> rule3))]
("Bob" "is" "red" "-")
((triple1) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((triple1) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is furry.
True
4
proof
[(((triple1 ((triple1) -> rule1)) -> rule5) OR ((triple1 ((triple1) -> rule3)) -> rule5))]
("Bob" "is" "furry" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
((triple1 ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is not furry.
False
4
inv-proof
[(((triple1 ((triple1) -> rule1)) -> rule5) OR ((triple1 ((triple1) -> rule3)) -> rule5))]
("Bob" "is" "furry" "-")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
((triple1 ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is cold.
True
5
proof
[(((((triple1 ((triple1) -> rule1)) -> rule5)) -> rule2) OR ((((triple1 ((triple1) -> rule3)) -> rule5)) -> rule2))]
("Bob" "is" "cold" "+")
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
((((triple1 ((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is not cold.
False
5
inv-proof
[(((((triple1 ((triple1) -> rule1)) -> rule5)) -> rule2) OR ((((triple1 ((triple1) -> rule3)) -> rule5)) -> rule2))]
("Bob" "is" "cold" "-")
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
((((triple1 ((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Fiona is not nice.
Unknown
inv-rconc
[@2: Fiona is nice.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("Fiona" "is" "nice" "-")
Bob is nice.
Unknown
rconc
[@1: Bob is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "nice" "+")
Gary is not furry.
Unknown
inv-rconc
[@1: Gary is furry.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "furry" "-")
Fiona is red.
Unknown
rconc
[@1: Fiona is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "red" "+")
Fiona is not round.
Unknown
inv-random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
Fiona is not green.
Unknown
inv-random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
@0: Bob is round.[(triple1)] Fiona is big.[(triple2)] Gary is big.[(triple3)] @1: Bob is red.[(((triple1) -> rule1) OR ((triple1) -> rule3))] @2: Bob is furry.[(((triple1 ((triple1) -> rule1)) -> rule5) OR ((triple1 ((triple1) -> rule3)) -> rule5))] @3: Bob is cold.[(((((triple1 ((triple1) -> rule1)) -> rule5)) -> rule2) OR ((((triple1 ((triple1) -> rule3)) -> rule5)) -> rule2))]
Bob is round.
("Bob" "is" "round" "+")
triple1
Fiona is big.
("Fiona" "is" "big" "+")
triple2
Gary is big.
("Gary" "is" "big" "+")
triple3
Bob is red.
("Bob" "is" "red" "+")
((triple1) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((triple1) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
((triple1 ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
((((triple1 ((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3