Charlie is red. Dave is not kind. Dave is not red. Dave is not white. Erin is blue. Harry is kind. Harry is red. Harry is round. Harry is white. Harry is young. All young things are red. Blue things are young.
Charlie is red.
("Charlie" "is" "red" "+")
Dave is not kind.
("Dave" "is" "kind" "-")
Dave is not red.
("Dave" "is" "red" "-")
Dave is not white.
("Dave" "is" "white" "-")
Erin is blue.
("Erin" "is" "blue" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
All young things are red.
((("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
Blue things are young.
((("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
Dave is not kind.
True
1
proof
[(triple2)]
("Dave" "is" "kind" "-")
triple2
Harry is not red.
False
1
inv-proof
[(triple7 OR ((triple10) -> rule1))]
("Harry" "is" "red" "-")
triple7
((triple10) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Erin is young.
True
2
proof
[(((triple5) -> rule2))]
("Erin" "is" "young" "+")
((triple5) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is not young.
False
2
inv-proof
[(((triple5) -> rule2))]
("Erin" "is" "young" "-")
((triple5) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is red.
True
3
proof
[(((((triple5) -> rule2)) -> rule1))]
("Erin" "is" "red" "+")
((((triple5) -> (rule2 % int2))) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is not red.
False
3
inv-proof
[(((((triple5) -> rule2)) -> rule1))]
("Erin" "is" "red" "-")
((((triple5) -> (rule2 % int2))) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Dave is not young.
Unknown
inv-rconc
[@1: Dave is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "young" "-")
Charlie is young.
Unknown
rconc
[@1: Charlie is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "young" "+")
Dave is not furry.
Unknown
inv-random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
Charlie is not white.
Unknown
inv-random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
@0: Charlie is red.[(triple1)] Dave is not kind.[(triple2)] Dave is not red.[(triple3)] Dave is not white.[(triple4)] Erin is blue.[(triple5)] Harry is kind.[(triple6)] Harry is red.[(triple7 OR ((triple10) -> rule1))] Harry is round.[(triple8)] Harry is white.[(triple9)] Harry is young.[(triple10)] @1: Erin is young.[(((triple5) -> rule2))] @2: Erin is red.[(((((triple5) -> rule2)) -> rule1))]
Charlie is red.
("Charlie" "is" "red" "+")
triple1
Dave is not kind.
("Dave" "is" "kind" "-")
triple2
Dave is not red.
("Dave" "is" "red" "-")
triple3
Dave is not white.
("Dave" "is" "white" "-")
triple4
Erin is blue.
("Erin" "is" "blue" "+")
triple5
Harry is kind.
("Harry" "is" "kind" "+")
triple6
Harry is red.
("Harry" "is" "red" "+")
triple7
((triple10) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
triple8
Harry is white.
("Harry" "is" "white" "+")
triple9
Harry is young.
("Harry" "is" "young" "+")
triple10
Erin is young.
("Erin" "is" "young" "+")
((triple5) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
((((triple5) -> (rule2 % int2))) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2