Anne is big. Anne is blue. Anne is green. Anne is kind. Anne is round. Bob is kind. Bob is round. Bob is not smart. Fiona is green. Fiona is round. Kind people are round. If Bob is quiet then Bob is not green. Round people are quiet. If someone is blue and not quiet then they are smart. If someone is big and not quiet then they are smart. If someone is smart and not quiet then they are not big.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is round.
("Anne" "is" "round" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is not smart.
("Bob" "is" "smart" "-")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Kind people are round.
((("someone" "is" "kind" "+")) -> ("someone" "is" "round" "+"))
If Bob is quiet then Bob is not green.
((("Bob" "is" "quiet" "+")) -> ("Bob" "is" "green" "-"))
Round people are quiet.
((("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
If someone is blue and not quiet then they are smart.
((("someone" "is" "blue" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "smart" "+"))
If someone is big and not quiet then they are smart.
((("someone" "is" "big" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "smart" "+"))
If someone is smart and not quiet then they are not big.
((("someone" "is" "smart" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "big" "-"))
Anne is big.
True
1
proof
[(triple1)]
("Anne" "is" "big" "+")
triple1
Anne is not big.
False
1
inv-proof
[(triple1)]
("Anne" "is" "big" "-")
triple1
Anne is quiet.
True
2
proof
[(((triple5) -> rule3) OR ((((triple4) -> rule1)) -> rule3))]
("Anne" "is" "quiet" "+")
((triple5) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Bob is not quiet.
False
2
inv-proof
[(((triple7) -> rule3) OR ((((triple6) -> rule1)) -> rule3))]
("Bob" "is" "quiet" "-")
((triple7) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((triple6) -> (rule1 % int2))) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is not green.
True
3
proof
[(((((triple7) -> rule3)) -> rule2) OR ((((((triple6) -> rule1)) -> rule3)) -> rule2))]
("Bob" "is" "green" "-")
((((triple7) -> (rule3 % int2))) -> (rule2 % int1))
Bob is not green.
("Bob" "is" "green" "-")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
((((((triple6) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Bob is not green.
("Bob" "is" "green" "-")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is green.
False
3
inv-proof
[(((((triple7) -> rule3)) -> rule2) OR ((((((triple6) -> rule1)) -> rule3)) -> rule2))]
("Bob" "is" "green" "+")
((((triple7) -> (rule3 % int2))) -> (rule2 % int1))
Bob is not green.
("Bob" "is" "green" "-")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
((((((triple6) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Bob is not green.
("Bob" "is" "green" "-")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Fiona is not smart.
Unknown
inv-rconc
[@1: Fiona is smart.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "smart" "-")
Anne is smart.
Unknown
rconc
[@1: Anne is smart.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "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" "+")
Fiona is not kind.
Unknown
inv-random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "-")
Fiona is blue.
Unknown
random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "+")
@0: Anne is big.[(triple1)] Anne is blue.[(triple2)] Anne is green.[(triple3)] Anne is kind.[(triple4)] Anne is round.[(triple5 OR ((triple4) -> rule1))] Bob is kind.[(triple6)] Bob is not smart.[(triple8)] Bob is round.[(triple7 OR ((triple6) -> rule1))] Fiona is green.[(triple9)] Fiona is round.[(triple10)] @1: Anne is quiet.[(((triple5) -> rule3) OR ((((triple4) -> rule1)) -> rule3))] Bob is quiet.[(((triple7) -> rule3) OR ((((triple6) -> rule1)) -> rule3))] Fiona is quiet.[(((triple10) -> rule3))] @2: Bob is not green.[(((((triple7) -> rule3)) -> rule2) OR ((((((triple6) -> rule1)) -> rule3)) -> rule2))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is green.
("Anne" "is" "green" "+")
triple3
Anne is kind.
("Anne" "is" "kind" "+")
triple4
Anne is round.
("Anne" "is" "round" "+")
triple5
((triple4) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
triple6
Bob is not smart.
("Bob" "is" "smart" "-")
triple8
Bob is round.
("Bob" "is" "round" "+")
triple7
((triple6) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
triple9
Fiona is round.
("Fiona" "is" "round" "+")
triple10
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple5) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple7) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((triple6) -> (rule1 % int2))) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple10) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Bob is not green.
("Bob" "is" "green" "-")
((((triple7) -> (rule3 % int2))) -> (rule2 % int1))
Bob is not green.
("Bob" "is" "green" "-")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
((((((triple6) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Bob is not green.
("Bob" "is" "green" "-")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3