Anne is big. Anne is red. Anne is round. Erin is big. Erin is green. Erin is round. Erin is smart. Fiona is not big. Fiona is quiet. Harry is quiet. Harry is smart. Smart people are big. Smart, big people are green. Green, round people are not red. If someone is quiet and blue then they are round. If Harry is big and Harry is green then Harry is blue. If Harry is not big then Harry is blue.
Anne is big.
("Anne" "is" "big" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is round.
("Anne" "is" "round" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Fiona is not big.
("Fiona" "is" "big" "-")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Smart people are big.
((("someone" "is" "smart" "+")) -> ("someone" "is" "big" "+"))
Smart, big people are green.
((("someone" "is" "smart" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
Green, round people are not red.
((("someone" "is" "green" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "red" "-"))
If someone is quiet and blue then they are round.
((("someone" "is" "quiet" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
If Harry is big and Harry is green then Harry is blue.
((("Harry" "is" "big" "+") ("Harry" "is" "green" "+")) -> ("Harry" "is" "blue" "+"))
If Harry is not big then Harry is blue.
((("Harry" "is" "big" "~")) -> ("Harry" "is" "blue" "+"))
Anne is red.
True
1
proof
[(triple2)]
("Anne" "is" "red" "+")
triple2
Harry is not quiet.
False
1
inv-proof
[(triple10)]
("Harry" "is" "quiet" "-")
triple10
Erin is not red.
True
3
proof
[(((triple5 triple6) -> rule3) OR ((((triple7 triple4) -> rule2) triple6) -> rule3) OR ((((triple7 ((triple7) -> rule1)) -> rule2) triple6) -> rule3))]
("Erin" "is" "red" "-")
((triple5 triple6) -> (rule3 % int1))
Erin is not red.
("Erin" "is" "red" "-")
int1
((((triple7 triple4) -> (rule2 % int2)) triple6) -> (rule3 % int1))
Erin is not red.
("Erin" "is" "red" "-")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
((((triple7 ((triple7) -> (rule1 % int3))) -> (rule2 % int2)) triple6) -> (rule3 % int1))
Erin is not red.
("Erin" "is" "red" "-")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Harry is not big.
False
2
inv-proof
[(((triple11) -> rule1))]
("Harry" "is" "big" "-")
((triple11) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is green.
True
4
proof
[(((triple11 ((triple11) -> rule1)) -> rule2))]
("Harry" "is" "green" "+")
((triple11 ((triple11) -> (rule1 % int2))) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is not green.
False
4
inv-proof
[(((triple11 ((triple11) -> rule1)) -> rule2))]
("Harry" "is" "green" "-")
((triple11 ((triple11) -> (rule1 % int2))) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is blue.
True
7
proof
[(((((triple11) -> rule1) ((triple11 ((triple11) -> rule1)) -> rule2)) -> rule5))]
("Harry" "is" "blue" "+")
((((triple11) -> (rule1 % int3)) ((triple11 ((triple11) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is not blue.
False
7
inv-proof
[(((((triple11) -> rule1) ((triple11 ((triple11) -> rule1)) -> rule2)) -> rule5))]
("Harry" "is" "blue" "-")
((((triple11) -> (rule1 % int3)) ((triple11 ((triple11) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is round.
True
9
proof
[(((triple10 ((((triple11) -> rule1) ((triple11 ((triple11) -> rule1)) -> rule2)) -> rule5)) -> rule4))]
("Harry" "is" "round" "+")
((triple10 ((((triple11) -> (rule1 % int4)) ((triple11 ((triple11) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4
Harry is not round.
False
9
inv-proof
[(((triple10 ((((triple11) -> rule1) ((triple11 ((triple11) -> rule1)) -> rule2)) -> rule5)) -> rule4))]
("Harry" "is" "round" "-")
((triple10 ((((triple11) -> (rule1 % int4)) ((triple11 ((triple11) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4
Harry is not red.
True
14
proof
[(((((triple11 ((triple11) -> rule1)) -> rule2) ((triple10 ((((triple11) -> rule1) ((triple11 ((triple11) -> rule1)) -> rule2)) -> rule5)) -> rule4)) -> rule3))]
("Harry" "is" "red" "-")
((((triple11 ((triple11) -> (rule1 % int5))) -> (rule2 % int4)) ((triple10 ((((triple11) -> (rule1 % int5)) ((triple11 ((triple11) -> (rule1 % int5))) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Harry is not red.
("Harry" "is" "red" "-")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
int4
Harry is big.
("Harry" "is" "big" "+")
int5
Harry is red.
False
14
inv-proof
[(((((triple11 ((triple11) -> rule1)) -> rule2) ((triple10 ((((triple11) -> rule1) ((triple11 ((triple11) -> rule1)) -> rule2)) -> rule5)) -> rule4)) -> rule3))]
("Harry" "is" "red" "+")
((((triple11 ((triple11) -> (rule1 % int5))) -> (rule2 % int4)) ((triple10 ((((triple11) -> (rule1 % int5)) ((triple11 ((triple11) -> (rule1 % int5))) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Harry is not red.
("Harry" "is" "red" "-")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
int4
Harry is big.
("Harry" "is" "big" "+")
int5
Anne is not green.
Unknown
inv-rconc
[@1: Anne is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "green" "-")
Fiona is green.
Unknown
rconc
[@1: Fiona is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "green" "+")
Fiona is not round.
Unknown
inv-rconc
[@1: Fiona is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "round" "-")
Fiona is red.
Unknown
random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "+")
Erin is not blue.
Unknown
inv-random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "-")
Fiona is blue.
Unknown
random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "+")
Fiona is not smart.
Unknown
inv-random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
Anne is not smart.
Unknown
inv-random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "-")
Erin is quiet.
Unknown
random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "+")
@0: Anne is big.[(triple1)] Anne is red.[(triple2)] Anne is round.[(triple3)] Erin is big.[(triple4 OR ((triple7) -> rule1))] Erin is green.[(triple5 OR ((triple7 triple4) -> rule2) OR ((triple7 ((triple7) -> rule1)) -> rule2))] Erin is round.[(triple6)] Erin is smart.[(triple7)] Fiona is not big.[(triple8)] Fiona is quiet.[(triple9)] Harry is quiet.[(triple10)] Harry is smart.[(triple11)] @1: Erin is not red.[(((triple5 triple6) -> rule3) OR ((((triple7 triple4) -> rule2) triple6) -> rule3) OR ((((triple7 ((triple7) -> rule1)) -> rule2) triple6) -> rule3))] Harry is big.[(((triple11) -> rule1))] @2: Harry is green.[(((triple11 ((triple11) -> rule1)) -> rule2))] @3: Harry is blue.[(((((triple11) -> rule1) ((triple11 ((triple11) -> rule1)) -> rule2)) -> rule5))] @4: Harry is round.[(((triple10 ((((triple11) -> rule1) ((triple11 ((triple11) -> rule1)) -> rule2)) -> rule5)) -> rule4))] @5: Harry is not red.[(((((triple11 ((triple11) -> rule1)) -> rule2) ((triple10 ((((triple11) -> rule1) ((triple11 ((triple11) -> rule1)) -> rule2)) -> rule5)) -> rule4)) -> rule3))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
Anne is round.
("Anne" "is" "round" "+")
triple3
Erin is big.
("Erin" "is" "big" "+")
triple4
((triple7) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
triple5
((triple7 triple4) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((triple7 ((triple7) -> (rule1 % int2))) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
triple6
Erin is smart.
("Erin" "is" "smart" "+")
triple7
Fiona is not big.
("Fiona" "is" "big" "-")
triple8
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple9
Harry is quiet.
("Harry" "is" "quiet" "+")
triple10
Harry is smart.
("Harry" "is" "smart" "+")
triple11
Erin is not red.
("Erin" "is" "red" "-")
((triple5 triple6) -> (rule3 % int1))
Erin is not red.
("Erin" "is" "red" "-")
int1
((((triple7 triple4) -> (rule2 % int2)) triple6) -> (rule3 % int1))
Erin is not red.
("Erin" "is" "red" "-")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
((((triple7 ((triple7) -> (rule1 % int3))) -> (rule2 % int2)) triple6) -> (rule3 % int1))
Erin is not red.
("Erin" "is" "red" "-")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
((triple11) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((triple11 ((triple11) -> (rule1 % int2))) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
((((triple11) -> (rule1 % int3)) ((triple11 ((triple11) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
((triple10 ((((triple11) -> (rule1 % int4)) ((triple11 ((triple11) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4
Harry is not red.
("Harry" "is" "red" "-")
((((triple11 ((triple11) -> (rule1 % int5))) -> (rule2 % int4)) ((triple10 ((((triple11) -> (rule1 % int5)) ((triple11 ((triple11) -> (rule1 % int5))) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Harry is not red.
("Harry" "is" "red" "-")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
int4
Harry is big.
("Harry" "is" "big" "+")
int5