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