Bob is cold. Bob is not green. Bob is not kind. Bob is not quiet. Erin is green. Erin is quiet. Fiona is cold. Fiona is green. Fiona is not kind. Fiona is smart. If something is green then it is furry. Green, big things are not quiet. If something is cold then it is smart. If something is kind and not furry then it is smart. All cold things are smart. All smart things are not kind. If something is cold and quiet then it is kind. If something is smart and not furry then it is kind.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is not green.
("Bob" "is" "green" "-")
Bob is not kind.
("Bob" "is" "kind" "-")
Bob is not quiet.
("Bob" "is" "quiet" "-")
Erin is green.
("Erin" "is" "green" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is not kind.
("Fiona" "is" "kind" "-")
Fiona is smart.
("Fiona" "is" "smart" "+")
If something is green then it is furry.
((("something" "is" "green" "+")) -> ("something" "is" "furry" "+"))
Green, big things are not quiet.
((("something" "is" "green" "+") ("something" "is" "big" "+")) -> ("something" "is" "quiet" "-"))
If something is cold then it is smart.
((("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
If something is kind and not furry then it is smart.
((("something" "is" "kind" "+") ("something" "is" "furry" "~")) -> ("something" "is" "smart" "+"))
All cold things are smart.
((("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
All smart things are not kind.
((("something" "is" "smart" "+")) -> ("something" "is" "kind" "-"))
If something is cold and quiet then it is kind.
((("something" "is" "cold" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "kind" "+"))
If something is smart and not furry then it is kind.
((("something" "is" "smart" "+") ("something" "is" "furry" "~")) -> ("something" "is" "kind" "+"))
Bob is cold.
True
1
proof
[(triple1)]
("Bob" "is" "cold" "+")
triple1
Bob is kind.
False
1
inv-proof
[(triple3 OR ((((triple1) -> rule3)) -> rule6) OR ((((triple1) -> rule5)) -> rule6))]
("Bob" "is" "kind" "+")
triple3
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
((((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Fiona is furry.
True
2
proof
[(((triple8) -> rule1))]
("Fiona" "is" "furry" "+")
((triple8) -> (rule1 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Erin is not furry.
False
2
inv-proof
[(((triple5) -> rule1))]
("Erin" "is" "furry" "-")
((triple5) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Bob is not furry.
Unknown
inv-rconc
[@1: Bob is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "furry" "-")
Erin is smart.
Unknown
rconc
[@1: Erin is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "smart" "+")
Fiona is not big.
Unknown
inv-random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
@0: Bob is cold.[(triple1)] Bob is not green.[(triple2)] Bob is not kind.[(triple3 OR ((((triple1) -> rule3)) -> rule6) OR ((((triple1) -> rule5)) -> rule6))] Bob is not quiet.[(triple4)] Erin is green.[(triple5)] Erin is quiet.[(triple6)] Fiona is cold.[(triple7)] Fiona is green.[(triple8)] Fiona is not kind.[(triple9 OR ((triple10) -> rule6) OR ((((triple7) -> rule3)) -> rule6) OR ((((triple7) -> rule5)) -> rule6))] Fiona is smart.[(triple10 OR ((triple7) -> rule3) OR ((triple7) -> rule5))] @1: Bob is smart.[(((triple1) -> rule3) OR ((triple1) -> rule5))] Erin is furry.[(((triple5) -> rule1))] Fiona is furry.[(((triple8) -> rule1))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is not green.
("Bob" "is" "green" "-")
triple2
Bob is not kind.
("Bob" "is" "kind" "-")
triple3
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
((((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is not quiet.
("Bob" "is" "quiet" "-")
triple4
Erin is green.
("Erin" "is" "green" "+")
triple5
Erin is quiet.
("Erin" "is" "quiet" "+")
triple6
Fiona is cold.
("Fiona" "is" "cold" "+")
triple7
Fiona is green.
("Fiona" "is" "green" "+")
triple8
Fiona is not kind.
("Fiona" "is" "kind" "-")
triple9
((triple10) -> (rule6 % int1))
Fiona is not kind.
("Fiona" "is" "kind" "-")
int1
((((triple7) -> (rule3 % int2))) -> (rule6 % int1))
Fiona is not kind.
("Fiona" "is" "kind" "-")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((((triple7) -> (rule5 % int2))) -> (rule6 % int1))
Fiona is not kind.
("Fiona" "is" "kind" "-")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
triple10
((triple7) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((triple7) -> (rule5 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((triple1) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((triple1) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((triple5) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
((triple8) -> (rule1 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1