Anne is blue. Bob is round. Fiona is green. Harry is round. If something is round and not green then it is red. Young, kind things are red. If something is blue then it is young. All round things are young. If something is round then it is kind. Round, red things are not blue.
Anne is blue.
("Anne" "is" "blue" "+")
Bob is round.
("Bob" "is" "round" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Harry is round.
("Harry" "is" "round" "+")
If something is round and not green then it is red.
((("something" "is" "round" "+") ("something" "is" "green" "~")) -> ("something" "is" "red" "+"))
Young, kind things are red.
((("something" "is" "young" "+") ("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
If something is blue then it is young.
((("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
All round things are young.
((("something" "is" "round" "+")) -> ("something" "is" "young" "+"))
If something is round then it is kind.
((("something" "is" "round" "+")) -> ("something" "is" "kind" "+"))
Round, red things are not blue.
((("something" "is" "round" "+") ("something" "is" "red" "+")) -> ("something" "is" "blue" "-"))
Fiona is green.
True
1
proof
[(triple3)]
("Fiona" "is" "green" "+")
triple3
Bob is not round.
False
1
inv-proof
[(triple2)]
("Bob" "is" "round" "-")
triple2
Harry is young.
True
2
proof
[(((triple4) -> rule4))]
("Harry" "is" "young" "+")
((triple4) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Bob is not young.
False
2
inv-proof
[(((triple2) -> rule4))]
("Bob" "is" "young" "-")
((triple2) -> (rule4 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is red.
True
5
proof
[(((((triple2) -> rule4) ((triple2) -> rule5)) -> rule2))]
("Bob" "is" "red" "+")
((((triple2) -> (rule4 % int3)) ((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Harry is not red.
False
5
inv-proof
[(((((triple4) -> rule4) ((triple4) -> rule5)) -> rule2))]
("Harry" "is" "red" "-")
((((triple4) -> (rule4 % int3)) ((triple4) -> (rule5 % int2))) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Bob is not blue.
True
7
proof
[(((triple2 ((((triple2) -> rule4) ((triple2) -> rule5)) -> rule2)) -> rule6))]
("Bob" "is" "blue" "-")
((triple2 ((((triple2) -> (rule4 % int4)) ((triple2) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Bob is not blue.
("Bob" "is" "blue" "-")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4
Harry is blue.
False
7
inv-proof
[(((triple4 ((((triple4) -> rule4) ((triple4) -> rule5)) -> rule2)) -> rule6))]
("Harry" "is" "blue" "+")
((triple4 ((((triple4) -> (rule4 % int4)) ((triple4) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Harry is not blue.
("Harry" "is" "blue" "-")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
int4
Anne is not kind.
Unknown
inv-rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "kind" "-")
Fiona is young.
Unknown
rconc
[@1: Fiona is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "young" "+")
Fiona is not kind.
Unknown
inv-rconc
[@1: Fiona is kind.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "kind" "-")
Anne is red.
Unknown
rconc
[@2: Anne is red.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("Anne" "is" "red" "+")
Anne is not green.
Unknown
inv-random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "-")
Fiona is nice.
Unknown
random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "+")
Harry is not nice.
Unknown
inv-random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "-")
Fiona is blue.
Unknown
random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "+")
@0: Anne is blue.[(triple1)] Bob is round.[(triple2)] Fiona is green.[(triple3)] Harry is round.[(triple4)] @1: Anne is young.[(((triple1) -> rule3))] Bob is kind.[(((triple2) -> rule5))] Bob is young.[(((triple2) -> rule4))] Harry is kind.[(((triple4) -> rule5))] Harry is young.[(((triple4) -> rule4))] @2: Bob is red.[(((((triple2) -> rule4) ((triple2) -> rule5)) -> rule2))] Harry is red.[(((((triple4) -> rule4) ((triple4) -> rule5)) -> rule2))] @3: Bob is not blue.[(((triple2 ((((triple2) -> rule4) ((triple2) -> rule5)) -> rule2)) -> rule6))] Harry is not blue.[(((triple4 ((((triple4) -> rule4) ((triple4) -> rule5)) -> rule2)) -> rule6))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Bob is round.
("Bob" "is" "round" "+")
triple2
Fiona is green.
("Fiona" "is" "green" "+")
triple3
Harry is round.
("Harry" "is" "round" "+")
triple4
Anne is young.
("Anne" "is" "young" "+")
((triple1) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((triple2) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
((triple2) -> (rule4 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((triple4) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple4) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
((((triple2) -> (rule4 % int3)) ((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Harry is red.
("Harry" "is" "red" "+")
((((triple4) -> (rule4 % int3)) ((triple4) -> (rule5 % int2))) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Bob is not blue.
("Bob" "is" "blue" "-")
((triple2 ((((triple2) -> (rule4 % int4)) ((triple2) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Bob is not blue.
("Bob" "is" "blue" "-")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4
Harry is not blue.
("Harry" "is" "blue" "-")
((triple4 ((((triple4) -> (rule4 % int4)) ((triple4) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Harry is not blue.
("Harry" "is" "blue" "-")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
int4