Anne is nice. Anne is smart. Dave is kind. Dave is nice. Dave is round. Fiona is smart. Harry is green. If Anne is nice then Anne is smart. If something is nice and green then it is red. Nice things are round. Smart things are green. All round, nice things are red. If something is smart and round then it is red.
Anne is nice.
("Anne" "is" "nice" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is round.
("Dave" "is" "round" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Harry is green.
("Harry" "is" "green" "+")
If Anne is nice then Anne is smart.
((("Anne" "is" "nice" "+")) -> ("Anne" "is" "smart" "+"))
If something is nice and green then it is red.
((("something" "is" "nice" "+") ("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
Nice things are round.
((("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
Smart things are green.
((("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
All round, nice things are red.
((("something" "is" "round" "+") ("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
If something is smart and round then it is red.
((("something" "is" "smart" "+") ("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
Dave is kind.
True
1
proof
[(triple3)]
("Dave" "is" "kind" "+")
triple3
Dave is not round.
False
1
inv-proof
[(triple5 OR ((triple4) -> rule3))]
("Dave" "is" "round" "-")
triple5
((triple4) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Anne is green.
True
2
proof
[(((triple2) -> rule4) OR ((((triple1) -> rule1)) -> rule4))]
("Anne" "is" "green" "+")
((triple2) -> (rule4 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Fiona is not green.
False
2
inv-proof
[(((triple6) -> rule4))]
("Fiona" "is" "green" "-")
((triple6) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Anne is red.
True
4
proof
[(((triple1 ((triple2) -> rule4)) -> rule2) OR ((triple2 ((triple1) -> rule3)) -> rule6) OR ((((triple1) -> rule3) triple1) -> rule5) OR ((((triple1) -> rule1) ((triple1) -> rule3)) -> rule6) OR ((triple1 ((((triple1) -> rule1)) -> rule4)) -> rule2))]
("Anne" "is" "red" "+")
((triple1 ((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
((triple2 ((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
((((triple1) -> (rule3 % int2)) triple1) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
((((triple1) -> (rule1 % int3)) ((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
((triple1 ((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is not red.
False
4
inv-proof
[(((triple1 ((triple2) -> rule4)) -> rule2) OR ((triple2 ((triple1) -> rule3)) -> rule6) OR ((((triple1) -> rule3) triple1) -> rule5) OR ((((triple1) -> rule1) ((triple1) -> rule3)) -> rule6) OR ((triple1 ((((triple1) -> rule1)) -> rule4)) -> rule2))]
("Anne" "is" "red" "-")
((triple1 ((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
((triple2 ((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
((((triple1) -> (rule3 % int2)) triple1) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
((((triple1) -> (rule1 % int3)) ((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
((triple1 ((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Harry is not round.
Unknown
inv-rconc
[@1: Harry is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "round" "-")
Fiona is red.
Unknown
rconc
[@2: Fiona is red.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("Fiona" "is" "red" "+")
Harry is not red.
Unknown
inv-rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "red" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
Anne is not young.
Unknown
inv-random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "-")
Anne is kind.
Unknown
random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "+")
@0: Anne is nice.[(triple1)] Anne is smart.[(triple2 OR ((triple1) -> rule1))] Dave is kind.[(triple3)] Dave is nice.[(triple4)] Dave is round.[(triple5 OR ((triple4) -> rule3))] Fiona is smart.[(triple6)] Harry is green.[(triple7)] @1: Anne is green.[(((triple2) -> rule4) OR ((((triple1) -> rule1)) -> rule4))] Anne is round.[(((triple1) -> rule3))] Dave is red.[(((triple5 triple4) -> rule5) OR ((((triple4) -> rule3) triple4) -> rule5))] Fiona is green.[(((triple6) -> rule4))] @2: Anne is red.[(((triple1 ((triple2) -> rule4)) -> rule2) OR ((triple2 ((triple1) -> rule3)) -> rule6) OR ((((triple1) -> rule3) triple1) -> rule5) OR ((((triple1) -> rule1) ((triple1) -> rule3)) -> rule6) OR ((triple1 ((((triple1) -> rule1)) -> rule4)) -> rule2))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Anne is smart.
("Anne" "is" "smart" "+")
triple2
((triple1) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
triple3
Dave is nice.
("Dave" "is" "nice" "+")
triple4
Dave is round.
("Dave" "is" "round" "+")
triple5
((triple4) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
triple6
Harry is green.
("Harry" "is" "green" "+")
triple7
Anne is green.
("Anne" "is" "green" "+")
((triple2) -> (rule4 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
((triple1) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
((triple5 triple4) -> (rule5 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((((triple4) -> (rule3 % int2)) triple4) -> (rule5 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
((triple6) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
((triple1 ((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
((triple2 ((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
((((triple1) -> (rule3 % int2)) triple1) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
((((triple1) -> (rule1 % int3)) ((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
((triple1 ((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3