Anne is green. Anne is red. Anne is smart. Anne is young. Dave is kind. Fiona is not blue. Fiona is red. Fiona is not young. Harry is not green. Harry is not kind. Harry is smart. Harry is young. All blue things are not green. Blue things are round. Kind things are young. All young, kind things are blue. If something is green then it is not kind. If something is round then it is red. All smart things are red. If something is red then it is smart. If Dave is green then Dave is round.
Anne is green.
("Anne" "is" "green" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is young.
("Anne" "is" "young" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Fiona is not blue.
("Fiona" "is" "blue" "-")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is not young.
("Fiona" "is" "young" "-")
Harry is not green.
("Harry" "is" "green" "-")
Harry is not kind.
("Harry" "is" "kind" "-")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is young.
("Harry" "is" "young" "+")
All blue things are not green.
((("something" "is" "blue" "+")) -> ("something" "is" "green" "-"))
Blue things are round.
((("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
Kind things are young.
((("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
All young, kind things are blue.
((("something" "is" "young" "+") ("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
If something is green then it is not kind.
((("something" "is" "green" "+")) -> ("something" "is" "kind" "-"))
If something is round then it is red.
((("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
All smart things are red.
((("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
If something is red then it is smart.
((("something" "is" "red" "+")) -> ("something" "is" "smart" "+"))
If Dave is green then Dave is round.
((("Dave" "is" "green" "+")) -> ("Dave" "is" "round" "+"))
Anne is smart.
True
1
proof
[(triple3 OR ((triple2) -> rule8))]
("Anne" "is" "smart" "+")
triple3
((triple2) -> (rule8 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Harry is kind.
False
1
inv-proof
[(triple10)]
("Harry" "is" "kind" "+")
triple10
Fiona is smart.
True
2
proof
[(((triple7) -> rule8))]
("Fiona" "is" "smart" "+")
((triple7) -> (rule8 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Dave is not young.
False
2
inv-proof
[(((triple5) -> rule3))]
("Dave" "is" "young" "-")
((triple5) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is blue.
True
4
proof
[(((((triple5) -> rule3) triple5) -> rule4))]
("Dave" "is" "blue" "+")
((((triple5) -> (rule3 % int2)) triple5) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is not blue.
False
4
inv-proof
[(((((triple5) -> rule3) triple5) -> rule4))]
("Dave" "is" "blue" "-")
((((triple5) -> (rule3 % int2)) triple5) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is round.
True
5
proof
[(((((((triple5) -> rule3) triple5) -> rule4)) -> rule2))]
("Dave" "is" "round" "+")
((((((triple5) -> (rule3 % int3)) triple5) -> (rule4 % int2))) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is not round.
False
5
inv-proof
[(((((((triple5) -> rule3) triple5) -> rule4)) -> rule2))]
("Dave" "is" "round" "-")
((((((triple5) -> (rule3 % int3)) triple5) -> (rule4 % int2))) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is red.
True
6
proof
[(((((((((triple5) -> rule3) triple5) -> rule4)) -> rule2)) -> rule6))]
("Dave" "is" "red" "+")
((((((((triple5) -> (rule3 % int4)) triple5) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
Dave is not red.
False
6
inv-proof
[(((((((((triple5) -> rule3) triple5) -> rule4)) -> rule2)) -> rule6))]
("Dave" "is" "red" "-")
((((((((triple5) -> (rule3 % int4)) triple5) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
Dave is smart.
True
7
proof
[(((((((((((triple5) -> rule3) triple5) -> rule4)) -> rule2)) -> rule6)) -> rule8))]
("Dave" "is" "smart" "+")
((((((((((triple5) -> (rule3 % int5)) triple5) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4
Dave is young.
("Dave" "is" "young" "+")
int5
Dave is not smart.
False
7
inv-proof
[(((((((((((triple5) -> rule3) triple5) -> rule4)) -> rule2)) -> rule6)) -> rule8))]
("Dave" "is" "smart" "-")
((((((((((triple5) -> (rule3 % int5)) triple5) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4
Dave is young.
("Dave" "is" "young" "+")
int5
Harry is not blue.
Unknown
inv-rconc
[@1: Harry is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "blue" "-")
Anne is round.
Unknown
rconc
[@2: Anne is round.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("Anne" "is" "round" "+")
Fiona is not round.
Unknown
inv-rconc
[@1: Fiona is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "round" "-")
Harry is round.
Unknown
rconc
[@2: Harry is round.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("Harry" "is" "round" "+")
Anne is not blue.
Unknown
inv-rconc
[@1: Anne is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "blue" "-")
Fiona is kind.
Unknown
random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "+")
@0: Anne is green.[(triple1)] Anne is red.[(triple2 OR ((triple3) -> rule7))] Anne is smart.[(triple3 OR ((triple2) -> rule8))] Anne is young.[(triple4)] Dave is kind.[(triple5)] Fiona is not blue.[(triple6)] Fiona is not young.[(triple8)] Fiona is red.[(triple7)] Harry is not green.[(triple9)] Harry is not kind.[(triple10)] Harry is smart.[(triple11)] Harry is young.[(triple12)] @1: Anne is not kind.[(((triple1) -> rule5))] Dave is young.[(((triple5) -> rule3))] Fiona is smart.[(((triple7) -> rule8))] Harry is red.[(((triple11) -> rule7))] @2: Dave is blue.[(((((triple5) -> rule3) triple5) -> rule4))] @3: Dave is not green.[(((((((triple5) -> rule3) triple5) -> rule4)) -> rule1))] Dave is round.[(((((((triple5) -> rule3) triple5) -> rule4)) -> rule2))] @4: Dave is red.[(((((((((triple5) -> rule3) triple5) -> rule4)) -> rule2)) -> rule6))] @5: Dave is smart.[(((((((((((triple5) -> rule3) triple5) -> rule4)) -> rule2)) -> rule6)) -> rule8))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
((triple3) -> (rule7 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
triple3
((triple2) -> (rule8 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
triple4
Dave is kind.
("Dave" "is" "kind" "+")
triple5
Fiona is not blue.
("Fiona" "is" "blue" "-")
triple6
Fiona is not young.
("Fiona" "is" "young" "-")
triple8
Fiona is red.
("Fiona" "is" "red" "+")
triple7
Harry is not green.
("Harry" "is" "green" "-")
triple9
Harry is not kind.
("Harry" "is" "kind" "-")
triple10
Harry is smart.
("Harry" "is" "smart" "+")
triple11
Harry is young.
("Harry" "is" "young" "+")
triple12
Anne is not kind.
("Anne" "is" "kind" "-")
((triple1) -> (rule5 % int1))
Anne is not kind.
("Anne" "is" "kind" "-")
int1
Dave is young.
("Dave" "is" "young" "+")
((triple5) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple7) -> (rule8 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple11) -> (rule7 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
((((triple5) -> (rule3 % int2)) triple5) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is not green.
("Dave" "is" "green" "-")
((((((triple5) -> (rule3 % int3)) triple5) -> (rule4 % int2))) -> (rule1 % int1))
Dave is not green.
("Dave" "is" "green" "-")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
((((((triple5) -> (rule3 % int3)) triple5) -> (rule4 % int2))) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
((((((((triple5) -> (rule3 % int4)) triple5) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
Dave is smart.
("Dave" "is" "smart" "+")
((((((((((triple5) -> (rule3 % int5)) triple5) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4
Dave is young.
("Dave" "is" "young" "+")
int5