Anne is white. Dave is big. Dave is green. Dave is smart. Erin is cold. Erin is green. Harry is white. All cold people are white. If someone is smart and kind then they are round. If someone is big then they are kind. White people are big. All kind people are smart.
Anne is white.
("Anne" "is" "white" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is green.
("Erin" "is" "green" "+")
Harry is white.
("Harry" "is" "white" "+")
All cold people are white.
((("someone" "is" "cold" "+")) -> ("someone" "is" "white" "+"))
If someone is smart and kind then they are round.
((("someone" "is" "smart" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "round" "+"))
If someone is big then they are kind.
((("someone" "is" "big" "+")) -> ("someone" "is" "kind" "+"))
White people are big.
((("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
All kind people are smart.
((("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
Anne is white.
True
1
proof
[(triple1)]
("Anne" "is" "white" "+")
triple1
Anne is not white.
False
1
inv-proof
[(triple1)]
("Anne" "is" "white" "-")
triple1
Erin is white.
True
2
proof
[(((triple5) -> rule1))]
("Erin" "is" "white" "+")
((triple5) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is not white.
False
2
inv-proof
[(((triple5) -> rule1))]
("Erin" "is" "white" "-")
((triple5) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Harry is kind.
True
3
proof
[(((((triple7) -> rule4)) -> rule3))]
("Harry" "is" "kind" "+")
((((triple7) -> (rule4 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Dave is not round.
False
4
inv-proof
[(((triple4 ((triple2) -> rule3)) -> rule2) OR ((((((triple2) -> rule3)) -> rule5) ((triple2) -> rule3)) -> rule2))]
("Dave" "is" "round" "-")
((triple4 ((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((((triple2) -> (rule3 % int3))) -> (rule5 % int2)) ((triple2) -> (rule3 % int3))) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Anne is smart.
True
4
proof
[(((((((triple1) -> rule4)) -> rule3)) -> rule5))]
("Anne" "is" "smart" "+")
((((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Harry is not smart.
False
4
inv-proof
[(((((((triple7) -> rule4)) -> rule3)) -> rule5))]
("Harry" "is" "smart" "-")
((((((triple7) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Erin is smart.
True
5
proof
[(((((((((triple5) -> rule1)) -> rule4)) -> rule3)) -> rule5))]
("Erin" "is" "smart" "+")
((((((((triple5) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
int4
Anne is not round.
False
8
inv-proof
[(((((((((triple1) -> rule4)) -> rule3)) -> rule5) ((((triple1) -> rule4)) -> rule3)) -> rule2))]
("Anne" "is" "round" "-")
((((((((triple1) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule5 % int2)) ((((triple1) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
int4
Erin is round.
True
10
proof
[(((((((((((triple5) -> rule1)) -> rule4)) -> rule3)) -> rule5) ((((((triple5) -> rule1)) -> rule4)) -> rule3)) -> rule2))]
("Erin" "is" "round" "+")
((((((((((triple5) -> (rule1 % int5))) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule5 % int2)) ((((((triple5) -> (rule1 % int5))) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
int4
Erin is white.
("Erin" "is" "white" "+")
int5
Erin is not round.
False
10
inv-proof
[(((((((((((triple5) -> rule1)) -> rule4)) -> rule3)) -> rule5) ((((((triple5) -> rule1)) -> rule4)) -> rule3)) -> rule2))]
("Erin" "is" "round" "-")
((((((((((triple5) -> (rule1 % int5))) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule5 % int2)) ((((((triple5) -> (rule1 % int5))) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
int4
Erin is white.
("Erin" "is" "white" "+")
int5
Dave is not white.
Unknown
inv-rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "white" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
Dave is not cold.
Unknown
inv-random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "-")
Anne is cold.
Unknown
random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "+")
Anne is not green.
Unknown
inv-random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
@0: Anne is white.[(triple1)] Dave is big.[(triple2)] Dave is green.[(triple3)] Dave is smart.[(triple4 OR ((((triple2) -> rule3)) -> rule5))] Erin is cold.[(triple5)] Erin is green.[(triple6)] Harry is white.[(triple7)] @1: Anne is big.[(((triple1) -> rule4))] Dave is kind.[(((triple2) -> rule3))] Erin is white.[(((triple5) -> rule1))] Harry is big.[(((triple7) -> rule4))] @2: Anne is kind.[(((((triple1) -> rule4)) -> rule3))] Dave is round.[(((triple4 ((triple2) -> rule3)) -> rule2) OR ((((((triple2) -> rule3)) -> rule5) ((triple2) -> rule3)) -> rule2))] Erin is big.[(((((triple5) -> rule1)) -> rule4))] Harry is kind.[(((((triple7) -> rule4)) -> rule3))] @3: Anne is smart.[(((((((triple1) -> rule4)) -> rule3)) -> rule5))] Erin is kind.[(((((((triple5) -> rule1)) -> rule4)) -> rule3))] Harry is smart.[(((((((triple7) -> rule4)) -> rule3)) -> rule5))] @4: Anne is round.[(((((((((triple1) -> rule4)) -> rule3)) -> rule5) ((((triple1) -> rule4)) -> rule3)) -> rule2))] Erin is smart.[(((((((((triple5) -> rule1)) -> rule4)) -> rule3)) -> rule5))] Harry is round.[(((((((((triple7) -> rule4)) -> rule3)) -> rule5) ((((triple7) -> rule4)) -> rule3)) -> rule2))] @5: Erin is round.[(((((((((((triple5) -> rule1)) -> rule4)) -> rule3)) -> rule5) ((((((triple5) -> rule1)) -> rule4)) -> rule3)) -> rule2))]
Anne is white.
("Anne" "is" "white" "+")
triple1
Dave is big.
("Dave" "is" "big" "+")
triple2
Dave is green.
("Dave" "is" "green" "+")
triple3
Dave is smart.
("Dave" "is" "smart" "+")
triple4
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
triple5
Erin is green.
("Erin" "is" "green" "+")
triple6
Harry is white.
("Harry" "is" "white" "+")
triple7
Anne is big.
("Anne" "is" "big" "+")
((triple1) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((triple2) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((triple5) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple7) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
((triple4 ((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((((triple2) -> (rule3 % int3))) -> (rule5 % int2)) ((triple2) -> (rule3 % int3))) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
((((triple5) -> (rule1 % int2))) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
((((triple7) -> (rule4 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
((((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
((((((triple5) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
((((((triple7) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
((((((((triple1) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule5 % int2)) ((((triple1) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
int4
Erin is smart.
("Erin" "is" "smart" "+")
((((((((triple5) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
int4
Harry is round.
("Harry" "is" "round" "+")
((((((((triple7) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule5 % int2)) ((((triple7) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4
Erin is round.
("Erin" "is" "round" "+")
((((((((((triple5) -> (rule1 % int5))) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule5 % int2)) ((((((triple5) -> (rule1 % int5))) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
int4
Erin is white.
("Erin" "is" "white" "+")
int5