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