Anne is green. Fiona is cold. Harry is big. If someone is green and quiet then they are cold. If someone is quiet then they are smart. Kind, big people are blue. If someone is quiet then they are green. If someone is big then they are quiet. If Harry is quiet then Harry is smart. Green, blue people are smart. Smart, quiet people are big.
Anne is green.
("Anne" "is" "green" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Harry is big.
("Harry" "is" "big" "+")
If someone is green and quiet then they are cold.
((("someone" "is" "green" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "cold" "+"))
If someone is quiet then they are smart.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
Kind, big people are blue.
((("someone" "is" "kind" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "blue" "+"))
If someone is quiet then they are green.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
If someone is big then they are quiet.
((("someone" "is" "big" "+")) -> ("someone" "is" "quiet" "+"))
If Harry is quiet then Harry is smart.
((("Harry" "is" "quiet" "+")) -> ("Harry" "is" "smart" "+"))
Green, blue people are smart.
((("someone" "is" "green" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "+"))
Smart, quiet people are big.
((("someone" "is" "smart" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "+"))
Harry is big.
True
1
proof
[(triple3)]
("Harry" "is" "big" "+")
triple3
Anne is not green.
False
1
inv-proof
[(triple1)]
("Anne" "is" "green" "-")
triple1
Harry is quiet.
True
2
proof
[(((triple3) -> rule5))]
("Harry" "is" "quiet" "+")
((triple3) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is not quiet.
False
2
inv-proof
[(((triple3) -> rule5))]
("Harry" "is" "quiet" "-")
((triple3) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is green.
True
3
proof
[(((((triple3) -> rule5)) -> rule4))]
("Harry" "is" "green" "+")
((((triple3) -> (rule5 % int2))) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is not green.
False
3
inv-proof
[(((((triple3) -> rule5)) -> rule4))]
("Harry" "is" "green" "-")
((((triple3) -> (rule5 % int2))) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is cold.
True
6
proof
[(((((((triple3) -> rule5)) -> rule4) ((triple3) -> rule5)) -> rule1))]
("Harry" "is" "cold" "+")
((((((triple3) -> (rule5 % int3))) -> (rule4 % int2)) ((triple3) -> (rule5 % int3))) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is not cold.
False
6
inv-proof
[(((((((triple3) -> rule5)) -> rule4) ((triple3) -> rule5)) -> rule1))]
("Harry" "is" "cold" "-")
((((((triple3) -> (rule5 % int3))) -> (rule4 % int2)) ((triple3) -> (rule5 % int3))) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Fiona is not blue.
Unknown
inv-rconc
[@1: Fiona is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "blue" "-")
Anne is cold.
Unknown
rconc
[@3: Anne is cold.[CWA. Example of deepest failure = (rule1 <- rule5 <- rule8 <- FAIL)]]
("Anne" "is" "cold" "+")
Fiona is not big.
Unknown
inv-rconc
[@2: Fiona is big.[CWA. Example of deepest failure = (rule8 <- rule5 <- FAIL)]]
("Fiona" "is" "big" "-")
Fiona is smart.
Unknown
rconc
[@3: Fiona is smart.[CWA. Example of deepest failure = (rule2 <- rule5 <- rule8 <- FAIL)]]
("Fiona" "is" "smart" "+")
Anne is not kind.
Unknown
inv-random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
@0: Anne is green.[(triple1)] Fiona is cold.[(triple2)] Harry is big.[(triple3)] @1: Harry is quiet.[(((triple3) -> rule5))] @2: Harry is green.[(((((triple3) -> rule5)) -> rule4))] Harry is smart.[(((((triple3) -> rule5)) -> rule2) OR ((((triple3) -> rule5)) -> rule6))] @3: Harry is cold.[(((((((triple3) -> rule5)) -> rule4) ((triple3) -> rule5)) -> rule1))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Fiona is cold.
("Fiona" "is" "cold" "+")
triple2
Harry is big.
("Harry" "is" "big" "+")
triple3
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple3) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((((triple3) -> (rule5 % int2))) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
((((triple3) -> (rule5 % int2))) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((triple3) -> (rule5 % int2))) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
((((((triple3) -> (rule5 % int3))) -> (rule4 % int2)) ((triple3) -> (rule5 % int3))) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3