Anne is big. Bob is quiet. Fiona is blue. Big, blue things are smart. If something is quiet and smart then it is blue. Blue things are smart. If Anne is quiet then Anne is blue. If something is nice and big then it is smart. All smart things are nice.
Anne is big.
("Anne" "is" "big" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Big, blue things are smart.
((("something" "is" "big" "+") ("something" "is" "blue" "+")) -> ("something" "is" "smart" "+"))
If something is quiet and smart then it is blue.
((("something" "is" "quiet" "+") ("something" "is" "smart" "+")) -> ("something" "is" "blue" "+"))
Blue things are smart.
((("something" "is" "blue" "+")) -> ("something" "is" "smart" "+"))
If Anne is quiet then Anne is blue.
((("Anne" "is" "quiet" "+")) -> ("Anne" "is" "blue" "+"))
If something is nice and big then it is smart.
((("something" "is" "nice" "+") ("something" "is" "big" "+")) -> ("something" "is" "smart" "+"))
All smart things are nice.
((("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
Anne is big.
True
1
proof
[(triple1)]
("Anne" "is" "big" "+")
triple1
Bob is not quiet.
False
1
inv-proof
[(triple2)]
("Bob" "is" "quiet" "-")
triple2
Fiona is smart.
True
2
proof
[(((triple3) -> rule3))]
("Fiona" "is" "smart" "+")
((triple3) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is not smart.
False
2
inv-proof
[(((triple3) -> rule3))]
("Fiona" "is" "smart" "-")
((triple3) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is nice.
True
3
proof
[(((((triple3) -> rule3)) -> rule6))]
("Fiona" "is" "nice" "+")
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is not nice.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule6))]
("Fiona" "is" "nice" "-")
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Anne is not smart.
Unknown
inv-rconc
[@4: Anne is smart.[CWA. Example of deepest failure = (rule5 <- rule6 <- rule1 <- rule2 <- FAIL)]]
("Anne" "is" "smart" "-")
Anne is nice.
Unknown
rconc
[@3: Anne is nice.[CWA. Example of deepest failure = (rule6 <- rule1 <- rule2 <- FAIL)]]
("Anne" "is" "nice" "+")
Bob is not nice.
Unknown
inv-rconc
[@4: Bob is nice.[CWA. Example of deepest failure = (rule6 <- rule3 <- rule2 <- rule1 <- FAIL)]]
("Bob" "is" "nice" "-")
Anne is quiet.
Unknown
random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "+")
Fiona is not furry.
Unknown
inv-random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
@0: Anne is big.[(triple1)] Bob is quiet.[(triple2)] Fiona is blue.[(triple3)] @1: Fiona is smart.[(((triple3) -> rule3))] @2: Fiona is nice.[(((((triple3) -> rule3)) -> rule6))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
Fiona is blue.
("Fiona" "is" "blue" "+")
triple3
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple3) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2