Charlie is cold. Dave is white. Erin is rough. Harry is cold. White things are red. All furry things are rough. If something is cold then it is rough. If Erin is not kind then Erin is cold. If something is red then it is cold. All rough, kind things are not nice. All rough, kind things are nice. If something is red and nice then it is not furry.
Charlie is cold.
("Charlie" "is" "cold" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Harry is cold.
("Harry" "is" "cold" "+")
White things are red.
((("something" "is" "white" "+")) -> ("something" "is" "red" "+"))
All furry things are rough.
((("something" "is" "furry" "+")) -> ("something" "is" "rough" "+"))
If something is cold then it is rough.
((("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
If Erin is not kind then Erin is cold.
((("Erin" "is" "kind" "~")) -> ("Erin" "is" "cold" "+"))
If something is red then it is cold.
((("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
All rough, kind things are not nice.
((("something" "is" "rough" "+") ("something" "is" "kind" "+")) -> ("something" "is" "nice" "-"))
All rough, kind things are nice.
((("something" "is" "rough" "+") ("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
If something is red and nice then it is not furry.
((("something" "is" "red" "+") ("something" "is" "nice" "+")) -> ("something" "is" "furry" "-"))
Charlie is cold.
True
1
proof
[(triple1)]
("Charlie" "is" "cold" "+")
triple1
Harry is not cold.
False
1
inv-proof
[(triple4)]
("Harry" "is" "cold" "-")
triple4
Harry is rough.
True
2
proof
[(((triple4) -> rule3))]
("Harry" "is" "rough" "+")
((triple4) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Charlie is not rough.
False
2
inv-proof
[(((triple1) -> rule3))]
("Charlie" "is" "rough" "-")
((triple1) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Dave is cold.
True
3
proof
[(((((triple2) -> rule1)) -> rule5))]
("Dave" "is" "cold" "+")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is not cold.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule5))]
("Dave" "is" "cold" "-")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is rough.
True
4
proof
[(((((((triple2) -> rule1)) -> rule5)) -> rule3))]
("Dave" "is" "rough" "+")
((((((triple2) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is not rough.
False
4
inv-proof
[(((((((triple2) -> rule1)) -> rule5)) -> rule3))]
("Dave" "is" "rough" "-")
((((((triple2) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Erin is not red.
Unknown
inv-rconc
[@1: Erin is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "red" "-")
Dave is nice.
Unknown
rconc
[@1: Dave is nice.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Dave" "is" "nice" "+")
Harry is not red.
Unknown
inv-rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "red" "-")
Charlie is red.
Unknown
rconc
[@1: Charlie is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "red" "+")
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
Erin is not furry.
Unknown
inv-random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
@0: Charlie is cold.[(triple1)] Dave is white.[(triple2)] Erin is rough.[(triple3)] Harry is cold.[(triple4)] @1: Charlie is rough.[(((triple1) -> rule3))] Dave is red.[(((triple2) -> rule1))] Harry is rough.[(((triple4) -> rule3))] @2: Dave is cold.[(((((triple2) -> rule1)) -> rule5))] @3: Dave is rough.[(((((((triple2) -> rule1)) -> rule5)) -> rule3))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Dave is white.
("Dave" "is" "white" "+")
triple2
Erin is rough.
("Erin" "is" "rough" "+")
triple3
Harry is cold.
("Harry" "is" "cold" "+")
triple4
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple1) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
((triple2) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple4) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
((((((triple2) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3