Anne is quiet. Anne is white. Dave is big. Dave is cold. Fiona is red. Harry is big. Harry is quiet. If something is big then it is young. All quiet, white things are big.
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is white.
("Anne" "is" "white" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
If something is big then it is young.
((("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
All quiet, white things are big.
((("something" "is" "quiet" "+") ("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
Dave is cold.
True
1
proof
[(triple4)]
("Dave" "is" "cold" "+")
triple4
Harry is not quiet.
False
1
inv-proof
[(triple7)]
("Harry" "is" "quiet" "-")
triple7
Anne is big.
True
3
proof
[(((triple1 triple2) -> rule2))]
("Anne" "is" "big" "+")
((triple1 triple2) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Dave is not young.
False
2
inv-proof
[(((triple3) -> rule1))]
("Dave" "is" "young" "-")
((triple3) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Anne is young.
True
4
proof
[(((((triple1 triple2) -> rule2)) -> rule1))]
("Anne" "is" "young" "+")
((((triple1 triple2) -> (rule2 % int2))) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is not young.
False
4
inv-proof
[(((((triple1 triple2) -> rule2)) -> rule1))]
("Anne" "is" "young" "-")
((((triple1 triple2) -> (rule2 % int2))) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Fiona is not young.
Unknown
inv-rconc
[@2: Fiona is young.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Fiona" "is" "young" "-")
Fiona is big.
Unknown
rconc
[@1: Fiona is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "big" "+")
Fiona is not blue.
Unknown
inv-random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "-")
Fiona is white.
Unknown
random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "+")
Harry is not blue.
Unknown
inv-random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
@0: Anne is quiet.[(triple1)] Anne is white.[(triple2)] Dave is big.[(triple3)] Dave is cold.[(triple4)] Fiona is red.[(triple5)] Harry is big.[(triple6)] Harry is quiet.[(triple7)] @1: Anne is big.[(((triple1 triple2) -> rule2))] Dave is young.[(((triple3) -> rule1))] Harry is young.[(((triple6) -> rule1))] @2: Anne is young.[(((((triple1 triple2) -> rule2)) -> rule1))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Anne is white.
("Anne" "is" "white" "+")
triple2
Dave is big.
("Dave" "is" "big" "+")
triple3
Dave is cold.
("Dave" "is" "cold" "+")
triple4
Fiona is red.
("Fiona" "is" "red" "+")
triple5
Harry is big.
("Harry" "is" "big" "+")
triple6
Harry is quiet.
("Harry" "is" "quiet" "+")
triple7
Anne is big.
("Anne" "is" "big" "+")
((triple1 triple2) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((triple3) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple6) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((((triple1 triple2) -> (rule2 % int2))) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2