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