Charlie is round. Dave is blue. Dave is quiet. All furry, red things are green. All round things are green. If something is furry and green then it is red. All green things are young. If Charlie is young and Charlie is furry then Charlie is red. If Dave is quiet and Dave is blue then Dave is round. All green, young things are quiet. Furry, green things are young.
Charlie is round.
("Charlie" "is" "round" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
All furry, red things are green.
((("something" "is" "furry" "+") ("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
All round things are green.
((("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
If something is furry and green then it is red.
((("something" "is" "furry" "+") ("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
All green things are young.
((("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
If Charlie is young and Charlie is furry then Charlie is red.
((("Charlie" "is" "young" "+") ("Charlie" "is" "furry" "+")) -> ("Charlie" "is" "red" "+"))
If Dave is quiet and Dave is blue then Dave is round.
((("Dave" "is" "quiet" "+") ("Dave" "is" "blue" "+")) -> ("Dave" "is" "round" "+"))
All green, young things are quiet.
((("something" "is" "green" "+") ("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
Furry, green things are young.
((("something" "is" "furry" "+") ("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
Dave is blue.
True
1
proof
[(triple2)]
("Dave" "is" "blue" "+")
triple2
Dave is not blue.
False
1
inv-proof
[(triple2)]
("Dave" "is" "blue" "-")
triple2
Dave is round.
True
3
proof
[(((triple3 triple2) -> rule6))]
("Dave" "is" "round" "+")
((triple3 triple2) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Charlie is not green.
False
2
inv-proof
[(((triple1) -> rule2))]
("Charlie" "is" "green" "-")
((triple1) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is young.
True
3
proof
[(((((triple1) -> rule2)) -> rule4))]
("Charlie" "is" "young" "+")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is not young.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule4))]
("Charlie" "is" "young" "-")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is quiet.
True
6
proof
[(((((triple1) -> rule2) ((((triple1) -> rule2)) -> rule4)) -> rule7))]
("Charlie" "is" "quiet" "+")
((((triple1) -> (rule2 % int3)) ((((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is not quiet.
False
6
inv-proof
[(((((triple1) -> rule2) ((((triple1) -> rule2)) -> rule4)) -> rule7))]
("Charlie" "is" "quiet" "-")
((((triple1) -> (rule2 % int3)) ((((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is not red.
Unknown
inv-rconc
[@1: Charlie is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "red" "-")
Dave is red.
Unknown
rconc
[@1: Dave is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "red" "+")
Charlie is not furry.
Unknown
inv-random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
@0: Charlie is round.[(triple1)] Dave is blue.[(triple2)] Dave is quiet.[(triple3)] @1: Charlie is green.[(((triple1) -> rule2))] Dave is round.[(((triple3 triple2) -> rule6))] @2: Charlie is young.[(((((triple1) -> rule2)) -> rule4))] Dave is green.[(((((triple3 triple2) -> rule6)) -> rule2))] @3: Charlie is quiet.[(((((triple1) -> rule2) ((((triple1) -> rule2)) -> rule4)) -> rule7))] Dave is young.[(((((((triple3 triple2) -> rule6)) -> rule2)) -> rule4))]
Charlie is round.
("Charlie" "is" "round" "+")
triple1
Dave is blue.
("Dave" "is" "blue" "+")
triple2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple3
Charlie is green.
("Charlie" "is" "green" "+")
((triple1) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((triple3 triple2) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
((((triple3 triple2) -> (rule6 % int2))) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((triple1) -> (rule2 % int3)) ((((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
((((((triple3 triple2) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3