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