Bob is nice. Charlie is not kind. Charlie is nice. Charlie is round. Dave is cold. Dave is young. Erin is cold. Erin is red. Erin is not round. Erin is young. Kind, nice things are cold. If something is red then it is cold. Nice things are round. If Bob is round and Bob is big then Bob is red. If something is round then it is big. Cold things are young. If Dave is big then Dave is cold. If Erin is young and Erin is kind then Erin is red.
Bob is nice.
("Bob" "is" "nice" "+")
Charlie is not kind.
("Charlie" "is" "kind" "-")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is not round.
("Erin" "is" "round" "-")
Erin is young.
("Erin" "is" "young" "+")
Kind, nice things are cold.
((("something" "is" "kind" "+") ("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
If something is red then it is cold.
((("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
Nice things are round.
((("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
If Bob is round and Bob is big then Bob is red.
((("Bob" "is" "round" "+") ("Bob" "is" "big" "+")) -> ("Bob" "is" "red" "+"))
If something is round then it is big.
((("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
Cold things are young.
((("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
If Dave is big then Dave is cold.
((("Dave" "is" "big" "+")) -> ("Dave" "is" "cold" "+"))
If Erin is young and Erin is kind then Erin is red.
((("Erin" "is" "young" "+") ("Erin" "is" "kind" "+")) -> ("Erin" "is" "red" "+"))
Dave is young.
True
1
proof
[(triple6 OR ((triple5) -> rule6))]
("Dave" "is" "young" "+")
triple6
((triple5) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Erin is not red.
False
1
inv-proof
[(triple8)]
("Erin" "is" "red" "-")
triple8
Charlie is big.
True
2
proof
[(((triple4) -> rule5) OR ((((triple3) -> rule3)) -> rule5))]
("Charlie" "is" "big" "+")
((triple4) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is not big.
False
2
inv-proof
[(((triple4) -> rule5) OR ((((triple3) -> rule3)) -> rule5))]
("Charlie" "is" "big" "-")
((triple4) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Bob is big.
True
3
proof
[(((((triple1) -> rule3)) -> rule5))]
("Bob" "is" "big" "+")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is not big.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule5))]
("Bob" "is" "big" "-")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is red.
True
6
proof
[(((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule5)) -> rule4))]
("Bob" "is" "red" "+")
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is not red.
False
6
inv-proof
[(((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule5)) -> rule4))]
("Bob" "is" "red" "-")
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is cold.
True
7
proof
[(((((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule5)) -> rule4)) -> rule2))]
("Bob" "is" "cold" "+")
((((((triple1) -> (rule3 % int4)) ((((triple1) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
int4
Bob is not cold.
False
7
inv-proof
[(((((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule5)) -> rule4)) -> rule2))]
("Bob" "is" "cold" "-")
((((((triple1) -> (rule3 % int4)) ((((triple1) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
int4
Bob is young.
True
8
proof
[(((((((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule5)) -> rule4)) -> rule2)) -> rule6))]
("Bob" "is" "young" "+")
((((((((triple1) -> (rule3 % int5)) ((((triple1) -> (rule3 % int5))) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
int4
Bob is round.
("Bob" "is" "round" "+")
int5
Bob is not young.
False
8
inv-proof
[(((((((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule5)) -> rule4)) -> rule2)) -> rule6))]
("Bob" "is" "young" "-")
((((((((triple1) -> (rule3 % int5)) ((((triple1) -> (rule3 % int5))) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
int4
Bob is round.
("Bob" "is" "round" "+")
int5
Erin is not big.
Unknown
inv-rconc
[@1: Erin is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "big" "-")
Charlie is young.
Unknown
rconc
[@2: Charlie is young.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Charlie" "is" "young" "+")
Dave is not big.
Unknown
inv-rconc
[@2: Dave is big.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("Dave" "is" "big" "-")
Charlie is cold.
Unknown
rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "cold" "+")
Dave is not round.
Unknown
inv-rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "round" "-")
Erin is nice.
Unknown
random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "+")
Charlie is not red.
Unknown
inv-random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
Dave is not red.
Unknown
inv-random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
@0: Bob is nice.[(triple1)] Charlie is nice.[(triple3)] Charlie is not kind.[(triple2)] Charlie is round.[(triple4 OR ((triple3) -> rule3))] Dave is cold.[(triple5)] Dave is young.[(triple6 OR ((triple5) -> rule6))] Erin is cold.[(triple7 OR ((triple8) -> rule2))] Erin is not round.[(triple9)] Erin is red.[(triple8)] Erin is young.[(triple10 OR ((triple7) -> rule6) OR ((((triple8) -> rule2)) -> rule6))] @1: Bob is round.[(((triple1) -> rule3))] Charlie is big.[(((triple4) -> rule5) OR ((((triple3) -> rule3)) -> rule5))] @2: Bob is big.[(((((triple1) -> rule3)) -> rule5))] @3: Bob is red.[(((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule5)) -> rule4))] @4: Bob is cold.[(((((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule5)) -> rule4)) -> rule2))] @5: Bob is young.[(((((((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule5)) -> rule4)) -> rule2)) -> rule6))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
Charlie is not kind.
("Charlie" "is" "kind" "-")
triple2
Charlie is round.
("Charlie" "is" "round" "+")
triple4
((triple3) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
triple5
Dave is young.
("Dave" "is" "young" "+")
triple6
((triple5) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
triple7
((triple8) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is not round.
("Erin" "is" "round" "-")
triple9
Erin is red.
("Erin" "is" "red" "+")
triple8
Erin is young.
("Erin" "is" "young" "+")
triple10
((triple7) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((((triple8) -> (rule2 % int2))) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
((triple1) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
((triple4) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
((((((triple1) -> (rule3 % int4)) ((((triple1) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
int4
Bob is young.
("Bob" "is" "young" "+")
((((((((triple1) -> (rule3 % int5)) ((((triple1) -> (rule3 % int5))) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
int4
Bob is round.
("Bob" "is" "round" "+")
int5