Charlie is white. Dave is red. Dave is young. Erin is cold. Erin is red. Gary is not white. Gary is young. Cold, red things are young. All white things are not rough. All white things are not rough. White things are cold. Cold, big things are red. If Charlie is white and Charlie is cold then Charlie is furry. All furry things are big. If something is cold then it is white. If Gary is rough and Gary is white then Gary is not red.
Charlie is white.
("Charlie" "is" "white" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is red.
("Erin" "is" "red" "+")
Gary is not white.
("Gary" "is" "white" "-")
Gary is young.
("Gary" "is" "young" "+")
Cold, red things are young.
((("something" "is" "cold" "+") ("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
All white things are not rough.
((("something" "is" "white" "+")) -> ("something" "is" "rough" "-"))
All white things are not rough.
((("something" "is" "white" "+")) -> ("something" "is" "rough" "-"))
White things are cold.
((("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
Cold, big things are red.
((("something" "is" "cold" "+") ("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
If Charlie is white and Charlie is cold then Charlie is furry.
((("Charlie" "is" "white" "+") ("Charlie" "is" "cold" "+")) -> ("Charlie" "is" "furry" "+"))
All furry things are big.
((("something" "is" "furry" "+")) -> ("something" "is" "big" "+"))
If something is cold then it is white.
((("something" "is" "cold" "+")) -> ("something" "is" "white" "+"))
If Gary is rough and Gary is white then Gary is not red.
((("Gary" "is" "rough" "+") ("Gary" "is" "white" "+")) -> ("Gary" "is" "red" "-"))
Dave is young.
True
1
proof
[(triple3)]
("Dave" "is" "young" "+")
triple3
Gary is not young.
False
1
inv-proof
[(triple7)]
("Gary" "is" "young" "-")
triple7
Charlie is not rough.
True
2
proof
[(((triple1) -> rule2) OR ((triple1) -> rule3))]
("Charlie" "is" "rough" "-")
((triple1) -> (rule2 % int1))
Charlie is not rough.
("Charlie" "is" "rough" "-")
int1
((triple1) -> (rule3 % int1))
Charlie is not rough.
("Charlie" "is" "rough" "-")
int1
Charlie is rough.
False
2
inv-proof
[(((triple1) -> rule2) OR ((triple1) -> rule3))]
("Charlie" "is" "rough" "+")
((triple1) -> (rule2 % int1))
Charlie is not rough.
("Charlie" "is" "rough" "-")
int1
((triple1) -> (rule3 % int1))
Charlie is not rough.
("Charlie" "is" "rough" "-")
int1
Charlie is furry.
True
4
proof
[(((triple1 ((triple1) -> rule4)) -> rule6))]
("Charlie" "is" "furry" "+")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is not furry.
False
4
inv-proof
[(((triple1 ((triple1) -> rule4)) -> rule6))]
("Charlie" "is" "furry" "-")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is big.
True
5
proof
[(((((triple1 ((triple1) -> rule4)) -> rule6)) -> rule7))]
("Charlie" "is" "big" "+")
((((triple1 ((triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is not big.
False
5
inv-proof
[(((((triple1 ((triple1) -> rule4)) -> rule6)) -> rule7))]
("Charlie" "is" "big" "-")
((((triple1 ((triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is red.
True
8
proof
[(((((triple1) -> rule4) ((((triple1 ((triple1) -> rule4)) -> rule6)) -> rule7)) -> rule5))]
("Charlie" "is" "red" "+")
((((triple1) -> (rule4 % int4)) ((((triple1 ((triple1) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is cold.
("Charlie" "is" "cold" "+")
int4
Charlie is not red.
False
8
inv-proof
[(((((triple1) -> rule4) ((((triple1 ((triple1) -> rule4)) -> rule6)) -> rule7)) -> rule5))]
("Charlie" "is" "red" "-")
((((triple1) -> (rule4 % int4)) ((((triple1 ((triple1) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is cold.
("Charlie" "is" "cold" "+")
int4
Charlie is young.
True
11
proof
[(((((triple1) -> rule4) ((((triple1) -> rule4) ((((triple1 ((triple1) -> rule4)) -> rule6)) -> rule7)) -> rule5)) -> rule1))]
("Charlie" "is" "young" "+")
((((triple1) -> (rule4 % int5)) ((((triple1) -> (rule4 % int5)) ((((triple1 ((triple1) -> (rule4 % int5))) -> (rule6 % int4))) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
int4
Charlie is cold.
("Charlie" "is" "cold" "+")
int5
Charlie is not young.
False
11
inv-proof
[(((((triple1) -> rule4) ((((triple1) -> rule4) ((((triple1 ((triple1) -> rule4)) -> rule6)) -> rule7)) -> rule5)) -> rule1))]
("Charlie" "is" "young" "-")
((((triple1) -> (rule4 % int5)) ((((triple1) -> (rule4 % int5)) ((((triple1 ((triple1) -> (rule4 % int5))) -> (rule6 % int4))) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
int4
Charlie is cold.
("Charlie" "is" "cold" "+")
int5
Gary is not red.
Unknown
inv-rconc
[@2: Gary is red.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("Gary" "is" "red" "-")
Dave is big.
Unknown
rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Dave" "is" "big" "+")
Gary is not cold.
Unknown
inv-rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "cold" "-")
Erin is big.
Unknown
rconc
[@1: Erin is big.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Erin" "is" "big" "+")
Gary is not big.
Unknown
inv-rconc
[@1: Gary is big.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Gary" "is" "big" "-")
Dave is white.
Unknown
rconc
[@2: Dave is white.[CWA. Example of deepest failure = (rule8 <- rule4 <- FAIL)]]
("Dave" "is" "white" "+")
Erin is not furry.
Unknown
inv-random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
Dave is not furry.
Unknown
inv-random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
@0: Charlie is white.[(triple1)] Dave is red.[(triple2)] Dave is young.[(triple3)] Erin is cold.[(triple4)] Erin is red.[(triple5)] Gary is not white.[(triple6)] Gary is young.[(triple7)] @1: Charlie is cold.[(((triple1) -> rule4))] Charlie is not rough.[(((triple1) -> rule2) OR ((triple1) -> rule3))] Erin is white.[(((triple4) -> rule8))] Erin is young.[(((triple4 triple5) -> rule1))] @2: Charlie is furry.[(((triple1 ((triple1) -> rule4)) -> rule6))] Erin is not rough.[(((((triple4) -> rule8)) -> rule2) OR ((((triple4) -> rule8)) -> rule3))] @3: Charlie is big.[(((((triple1 ((triple1) -> rule4)) -> rule6)) -> rule7))] @4: Charlie is red.[(((((triple1) -> rule4) ((((triple1 ((triple1) -> rule4)) -> rule6)) -> rule7)) -> rule5))] @5: Charlie is young.[(((((triple1) -> rule4) ((((triple1) -> rule4) ((((triple1 ((triple1) -> rule4)) -> rule6)) -> rule7)) -> rule5)) -> rule1))]
Charlie is white.
("Charlie" "is" "white" "+")
triple1
Dave is red.
("Dave" "is" "red" "+")
triple2
Dave is young.
("Dave" "is" "young" "+")
triple3
Erin is cold.
("Erin" "is" "cold" "+")
triple4
Erin is red.
("Erin" "is" "red" "+")
triple5
Gary is not white.
("Gary" "is" "white" "-")
triple6
Gary is young.
("Gary" "is" "young" "+")
triple7
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple1) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is not rough.
("Charlie" "is" "rough" "-")
((triple1) -> (rule2 % int1))
Charlie is not rough.
("Charlie" "is" "rough" "-")
int1
((triple1) -> (rule3 % int1))
Charlie is not rough.
("Charlie" "is" "rough" "-")
int1
Erin is white.
("Erin" "is" "white" "+")
((triple4) -> (rule8 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
((triple4 triple5) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Erin is not rough.
("Erin" "is" "rough" "-")
((((triple4) -> (rule8 % int2))) -> (rule2 % int1))
Erin is not rough.
("Erin" "is" "rough" "-")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((((triple4) -> (rule8 % int2))) -> (rule3 % int1))
Erin is not rough.
("Erin" "is" "rough" "-")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
((((triple1 ((triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is red.
("Charlie" "is" "red" "+")
((((triple1) -> (rule4 % int4)) ((((triple1 ((triple1) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is cold.
("Charlie" "is" "cold" "+")
int4
Charlie is young.
("Charlie" "is" "young" "+")
((((triple1) -> (rule4 % int5)) ((((triple1) -> (rule4 % int5)) ((((triple1 ((triple1) -> (rule4 % int5))) -> (rule6 % int4))) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
int4
Charlie is cold.
("Charlie" "is" "cold" "+")
int5