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