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