Anne is red. Bob is kind. Bob is not round. Dave is green. Dave is red. Dave is round. Dave is young. Fiona is blue. Fiona is not rough. Fiona is round. If something is green and kind then it is not red. All round things are red. All rough, kind things are not red. If something is round then it is young. If something is rough and red then it is green. If Fiona is young then Fiona is kind. Round things are blue. Rough, blue things are not kind.
Anne is red.
("Anne" "is" "red" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is not round.
("Bob" "is" "round" "-")
Dave is green.
("Dave" "is" "green" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is young.
("Dave" "is" "young" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is not rough.
("Fiona" "is" "rough" "-")
Fiona is round.
("Fiona" "is" "round" "+")
If something is green and kind then it is not red.
((("something" "is" "green" "+") ("something" "is" "kind" "+")) -> ("something" "is" "red" "-"))
All round things are red.
((("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
All rough, kind things are not red.
((("something" "is" "rough" "+") ("something" "is" "kind" "+")) -> ("something" "is" "red" "-"))
If something is round then it is young.
((("something" "is" "round" "+")) -> ("something" "is" "young" "+"))
If something is rough and red then it is green.
((("something" "is" "rough" "+") ("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
If Fiona is young then Fiona is kind.
((("Fiona" "is" "young" "+")) -> ("Fiona" "is" "kind" "+"))
Round things are blue.
((("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
Rough, blue things are not kind.
((("something" "is" "rough" "+") ("something" "is" "blue" "+")) -> ("something" "is" "kind" "-"))
Bob is kind.
True
1
proof
[(triple2)]
("Bob" "is" "kind" "+")
triple2
Fiona is not blue.
False
1
inv-proof
[(triple8 OR ((triple10) -> rule7))]
("Fiona" "is" "blue" "-")
triple8
((triple10) -> (rule7 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Dave is blue.
True
2
proof
[(((triple6) -> rule7))]
("Dave" "is" "blue" "+")
((triple6) -> (rule7 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is not blue.
False
2
inv-proof
[(((triple6) -> rule7))]
("Dave" "is" "blue" "-")
((triple6) -> (rule7 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Fiona is kind.
True
3
proof
[(((((triple10) -> rule4)) -> rule6))]
("Fiona" "is" "kind" "+")
((((triple10) -> (rule4 % int2))) -> (rule6 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is not kind.
False
3
inv-proof
[(((((triple10) -> rule4)) -> rule6))]
("Fiona" "is" "kind" "-")
((((triple10) -> (rule4 % int2))) -> (rule6 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Bob is not blue.
Unknown
inv-rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Bob" "is" "blue" "-")
Bob is young.
Unknown
rconc
[@1: Bob is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "young" "+")
Bob is not green.
Unknown
inv-rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "green" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
Anne is not kind.
Unknown
inv-random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "-")
Anne is round.
Unknown
random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "+")
@0: Anne is red.[(triple1)] Bob is kind.[(triple2)] Bob is not round.[(triple3)] Dave is green.[(triple4)] Dave is red.[(triple5 OR ((triple6) -> rule2))] Dave is round.[(triple6)] Dave is young.[(triple7 OR ((triple6) -> rule4))] Fiona is blue.[(triple8 OR ((triple10) -> rule7))] Fiona is not rough.[(triple9)] Fiona is round.[(triple10)] @1: Dave is blue.[(((triple6) -> rule7))] Fiona is red.[(((triple10) -> rule2))] Fiona is young.[(((triple10) -> rule4))] @2: Fiona is kind.[(((((triple10) -> rule4)) -> rule6))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Bob is not round.
("Bob" "is" "round" "-")
triple3
Dave is green.
("Dave" "is" "green" "+")
triple4
Dave is red.
("Dave" "is" "red" "+")
triple5
((triple6) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
triple6
Dave is young.
("Dave" "is" "young" "+")
triple7
((triple6) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
triple8
((triple10) -> (rule7 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is not rough.
("Fiona" "is" "rough" "-")
triple9
Fiona is round.
("Fiona" "is" "round" "+")
triple10
Dave is blue.
("Dave" "is" "blue" "+")
((triple6) -> (rule7 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
((triple10) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
((triple10) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
((((triple10) -> (rule4 % int2))) -> (rule6 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2