Charlie is blue. Dave is big. Dave is blue. All big, kind things are nice. If Dave is smart then Dave is kind. Big things are red. If something is white then it is nice. If something is nice then it is smart. All blue things are kind.
Charlie is blue.
("Charlie" "is" "blue" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
All big, kind things are nice.
((("something" "is" "big" "+") ("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
If Dave is smart then Dave is kind.
((("Dave" "is" "smart" "+")) -> ("Dave" "is" "kind" "+"))
Big things are red.
((("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
If something is white then it is nice.
((("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
If something is nice then it is smart.
((("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
All blue things are kind.
((("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
Dave is blue.
True
1
proof
[(triple3)]
("Dave" "is" "blue" "+")
triple3
Charlie is not blue.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "blue" "-")
triple1
Charlie is kind.
True
2
proof
[(((triple1) -> rule6))]
("Charlie" "is" "kind" "+")
((triple1) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is not kind.
False
2
inv-proof
[(((triple1) -> rule6))]
("Charlie" "is" "kind" "-")
((triple1) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Dave is nice.
True
4
proof
[(((triple2 ((triple3) -> rule6)) -> rule1))]
("Dave" "is" "nice" "+")
((triple2 ((triple3) -> (rule6 % int2))) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is not nice.
False
4
inv-proof
[(((triple2 ((triple3) -> rule6)) -> rule1))]
("Dave" "is" "nice" "-")
((triple2 ((triple3) -> (rule6 % int2))) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is smart.
True
5
proof
[(((((triple2 ((triple3) -> rule6)) -> rule1)) -> rule5))]
("Dave" "is" "smart" "+")
((((triple2 ((triple3) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is not smart.
False
5
inv-proof
[(((((triple2 ((triple3) -> rule6)) -> rule1)) -> rule5))]
("Dave" "is" "smart" "-")
((((triple2 ((triple3) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Charlie is not red.
Unknown
inv-rconc
[@1: Charlie is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "red" "-")
Charlie is nice.
Unknown
rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "nice" "+")
Charlie is not smart.
Unknown
inv-rconc
[@2: Charlie is smart.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Charlie" "is" "smart" "-")
Charlie is white.
Unknown
random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "+")
Charlie is not big.
Unknown
inv-random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
@0: Charlie is blue.[(triple1)] Dave is big.[(triple2)] Dave is blue.[(triple3)] @1: Charlie is kind.[(((triple1) -> rule6))] Dave is kind.[(((triple3) -> rule6))] Dave is red.[(((triple2) -> rule3))] @2: Dave is nice.[(((triple2 ((triple3) -> rule6)) -> rule1))] @3: Dave is smart.[(((((triple2 ((triple3) -> rule6)) -> rule1)) -> rule5))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Dave is big.
("Dave" "is" "big" "+")
triple2
Dave is blue.
("Dave" "is" "blue" "+")
triple3
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple1) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((triple3) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
((triple2) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((triple2 ((triple3) -> (rule6 % int2))) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
((((triple2 ((triple3) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3