Anne is blue. Anne is red. Anne is smart. Bob is not big. Bob is quiet. Bob is red. Fiona is furry. Fiona is green. Fiona is not quiet. Harry is furry. Harry is green. Harry is smart. If someone is green and not quiet then they are smart. If someone is red and not quiet then they are blue. If someone is big and not quiet then they are blue. All smart people are big. If someone is red and not quiet then they are furry. If someone is big then they are furry.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Bob is not big.
("Bob" "is" "big" "-")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If someone is green and not quiet then they are smart.
((("someone" "is" "green" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "smart" "+"))
If someone is red and not quiet then they are blue.
((("someone" "is" "red" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "blue" "+"))
If someone is big and not quiet then they are blue.
((("someone" "is" "big" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "blue" "+"))
All smart people are big.
((("someone" "is" "smart" "+")) -> ("someone" "is" "big" "+"))
If someone is red and not quiet then they are furry.
((("someone" "is" "red" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "furry" "+"))
If someone is big then they are furry.
((("someone" "is" "big" "+")) -> ("someone" "is" "furry" "+"))
Fiona is green.
True
1
proof
[(triple8)]
("Fiona" "is" "green" "+")
triple8
Harry is not smart.
False
1
inv-proof
[(triple12)]
("Harry" "is" "smart" "-")
triple12
Anne is big.
True
2
proof
[(((triple3) -> rule4))]
("Anne" "is" "big" "+")
((triple3) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is not big.
False
2
inv-proof
[(((triple3) -> rule4))]
("Anne" "is" "big" "-")
((triple3) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Fiona is big.
True
4
proof
[(((((triple8 triple9) -> rule1)) -> rule4))]
("Fiona" "is" "big" "+")
((((triple8 triple9) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Anne is not furry.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule6))]
("Anne" "is" "furry" "-")
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Fiona is blue.
True
6
proof
[(((((((triple8 triple9) -> rule1)) -> rule4) triple9) -> rule3))]
("Fiona" "is" "blue" "+")
((((((triple8 triple9) -> (rule1 % int3))) -> (rule4 % int2)) triple9) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is not blue.
False
6
inv-proof
[(((((((triple8 triple9) -> rule1)) -> rule4) triple9) -> rule3))]
("Fiona" "is" "blue" "-")
((((((triple8 triple9) -> (rule1 % int3))) -> (rule4 % int2)) triple9) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Bob is not blue.
Unknown
inv-rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "blue" "-")
Bob is smart.
Unknown
rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "smart" "+")
Bob is not furry.
Unknown
inv-rconc
[@1: Bob is furry.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "furry" "-")
Harry is blue.
Unknown
rconc
[@1: Harry is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "blue" "+")
Anne is not quiet.
Unknown
inv-random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
Harry is not quiet.
Unknown
inv-random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "-")
Fiona is red.
Unknown
random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "+")
@0: Anne is blue.[(triple1)] Anne is red.[(triple2)] Anne is smart.[(triple3)] Bob is not big.[(triple4)] Bob is quiet.[(triple5)] Bob is red.[(triple6)] Fiona is furry.[(triple7 OR ((((((triple8 triple9) -> rule1)) -> rule4)) -> rule6))] Fiona is green.[(triple8)] Fiona is not quiet.[(triple9)] Harry is furry.[(triple10 OR ((((triple12) -> rule4)) -> rule6))] Harry is green.[(triple11)] Harry is smart.[(triple12)] @1: Anne is big.[(((triple3) -> rule4))] Fiona is smart.[(((triple8 triple9) -> rule1))] Harry is big.[(((triple12) -> rule4))] @2: Anne is furry.[(((((triple3) -> rule4)) -> rule6))] Fiona is big.[(((((triple8 triple9) -> rule1)) -> rule4))] @3: Fiona is blue.[(((((((triple8 triple9) -> rule1)) -> rule4) triple9) -> rule3))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
Anne is smart.
("Anne" "is" "smart" "+")
triple3
Bob is not big.
("Bob" "is" "big" "-")
triple4
Bob is quiet.
("Bob" "is" "quiet" "+")
triple5
Bob is red.
("Bob" "is" "red" "+")
triple6
Fiona is furry.
("Fiona" "is" "furry" "+")
triple7
((((((triple8 triple9) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
triple8
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
triple9
Harry is furry.
("Harry" "is" "furry" "+")
triple10
((((triple12) -> (rule4 % int2))) -> (rule6 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
triple11
Harry is smart.
("Harry" "is" "smart" "+")
triple12
Anne is big.
("Anne" "is" "big" "+")
((triple3) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple8 triple9) -> (rule1 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple12) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
((((triple8 triple9) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
((((((triple8 triple9) -> (rule1 % int3))) -> (rule4 % int2)) triple9) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3