Anne is big. Anne is furry. Anne is green. Bob is quiet. Fiona is big. Fiona is furry. Fiona is smart. All big, smart things are green. If Anne is green and Anne is blue then Anne is big. All round, blue things are green. If Fiona is big then Fiona is furry. If Anne is green and Anne is quiet then Anne is round. All furry things are big.
Anne is big.
("Anne" "is" "big" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is green.
("Anne" "is" "green" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
All big, smart things are green.
((("something" "is" "big" "+") ("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
If Anne is green and Anne is blue then Anne is big.
((("Anne" "is" "green" "+") ("Anne" "is" "blue" "+")) -> ("Anne" "is" "big" "+"))
All round, blue things are green.
((("something" "is" "round" "+") ("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
If Fiona is big then Fiona is furry.
((("Fiona" "is" "big" "+")) -> ("Fiona" "is" "furry" "+"))
If Anne is green and Anne is quiet then Anne is round.
((("Anne" "is" "green" "+") ("Anne" "is" "quiet" "+")) -> ("Anne" "is" "round" "+"))
All furry things are big.
((("something" "is" "furry" "+")) -> ("something" "is" "big" "+"))
Fiona is big.
True
1
proof
[(triple5 OR ((triple6) -> rule6))]
("Fiona" "is" "big" "+")
triple5
((triple6) -> (rule6 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Bob is not quiet.
False
1
inv-proof
[(triple4)]
("Bob" "is" "quiet" "-")
triple4
Fiona is green.
True
3
proof
[(((triple5 triple7) -> rule1) OR ((((triple6) -> rule6) triple7) -> rule1))]
("Fiona" "is" "green" "+")
((triple5 triple7) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
((((triple6) -> (rule6 % int2)) triple7) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is not green.
False
3
inv-proof
[(((triple5 triple7) -> rule1) OR ((((triple6) -> rule6) triple7) -> rule1))]
("Fiona" "is" "green" "-")
((triple5 triple7) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
((((triple6) -> (rule6 % int2)) triple7) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Bob is not green.
Unknown
inv-rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "green" "-")
Bob is big.
Unknown
rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "big" "+")
Bob is not round.
Unknown
inv-random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "-")
Anne is quiet.
Unknown
random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "+")
@0: Anne is big.[(triple1 OR ((triple2) -> rule6))] Anne is furry.[(triple2)] Anne is green.[(triple3)] Bob is quiet.[(triple4)] Fiona is big.[(triple5 OR ((triple6) -> rule6))] Fiona is furry.[(triple6 OR ((triple5) -> rule4))] Fiona is smart.[(triple7)] @1: Fiona is green.[(((triple5 triple7) -> rule1) OR ((((triple6) -> rule6) triple7) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple2) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Anne is green.
("Anne" "is" "green" "+")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
Fiona is big.
("Fiona" "is" "big" "+")
triple5
((triple6) -> (rule6 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
triple6
((triple5) -> (rule4 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
triple7
Fiona is green.
("Fiona" "is" "green" "+")
((triple5 triple7) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
((((triple6) -> (rule6 % int2)) triple7) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2