Charlie is young. Dave is young. Gary is big. If someone is kind then they are quiet. If someone is big then they are young. If someone is round then they are quiet. If someone is blue and round then they are young. If Charlie is quiet and Charlie is kind then Charlie is smart. All blue people are kind. All young people are blue. Quiet, smart people are round.
Charlie is young.
("Charlie" "is" "young" "+")
Dave is young.
("Dave" "is" "young" "+")
Gary is big.
("Gary" "is" "big" "+")
If someone is kind then they are quiet.
((("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "+"))
If someone is big then they are young.
((("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
If someone is round then they are quiet.
((("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
If someone is blue and round then they are young.
((("someone" "is" "blue" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
If Charlie is quiet and Charlie is kind then Charlie is smart.
((("Charlie" "is" "quiet" "+") ("Charlie" "is" "kind" "+")) -> ("Charlie" "is" "smart" "+"))
All blue people are kind.
((("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
All young people are blue.
((("someone" "is" "young" "+")) -> ("someone" "is" "blue" "+"))
Quiet, smart people are round.
((("someone" "is" "quiet" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "round" "+"))
Gary is big.
True
1
proof
[(triple3)]
("Gary" "is" "big" "+")
triple3
Dave is not young.
False
1
inv-proof
[(triple2)]
("Dave" "is" "young" "-")
triple2
Dave is blue.
True
2
proof
[(((triple2) -> rule7))]
("Dave" "is" "blue" "+")
((triple2) -> (rule7 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Gary is not young.
False
2
inv-proof
[(((triple3) -> rule2))]
("Gary" "is" "young" "-")
((triple3) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is blue.
True
3
proof
[(((((triple3) -> rule2)) -> rule7))]
("Gary" "is" "blue" "+")
((((triple3) -> (rule2 % int2))) -> (rule7 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Dave is not kind.
False
3
inv-proof
[(((((triple2) -> rule7)) -> rule6))]
("Dave" "is" "kind" "-")
((((triple2) -> (rule7 % int2))) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Gary is kind.
True
4
proof
[(((((((triple3) -> rule2)) -> rule7)) -> rule6))]
("Gary" "is" "kind" "+")
((((((triple3) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Charlie is not quiet.
False
4
inv-proof
[(((((((triple1) -> rule7)) -> rule6)) -> rule1))]
("Charlie" "is" "quiet" "-")
((((((triple1) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Dave is not round.
Unknown
inv-rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Dave" "is" "round" "-")
Gary is round.
Unknown
rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Gary" "is" "round" "+")
Gary is not smart.
Unknown
inv-random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
Charlie is not big.
Unknown
inv-random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
@0: Charlie is young.[(triple1)] Dave is young.[(triple2)] Gary is big.[(triple3)] @1: Charlie is blue.[(((triple1) -> rule7))] Dave is blue.[(((triple2) -> rule7))] Gary is young.[(((triple3) -> rule2))] @2: Charlie is kind.[(((((triple1) -> rule7)) -> rule6))] Dave is kind.[(((((triple2) -> rule7)) -> rule6))] Gary is blue.[(((((triple3) -> rule2)) -> rule7))] @3: Charlie is quiet.[(((((((triple1) -> rule7)) -> rule6)) -> rule1))] Dave is quiet.[(((((((triple2) -> rule7)) -> rule6)) -> rule1))] Gary is kind.[(((((((triple3) -> rule2)) -> rule7)) -> rule6))] @4: Charlie is smart.[(((((((((triple1) -> rule7)) -> rule6)) -> rule1) ((((triple1) -> rule7)) -> rule6)) -> rule5))] Gary is quiet.[(((((((((triple3) -> rule2)) -> rule7)) -> rule6)) -> rule1))] @5: Charlie is round.[(((((((((triple1) -> rule7)) -> rule6)) -> rule1) ((((((((triple1) -> rule7)) -> rule6)) -> rule1) ((((triple1) -> rule7)) -> rule6)) -> rule5)) -> rule8))]
Charlie is young.
("Charlie" "is" "young" "+")
triple1
Dave is young.
("Dave" "is" "young" "+")
triple2
Gary is big.
("Gary" "is" "big" "+")
triple3
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple1) -> (rule7 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
((triple2) -> (rule7 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((triple3) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((((triple1) -> (rule7 % int2))) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
((((triple2) -> (rule7 % int2))) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
((((triple3) -> (rule2 % int2))) -> (rule7 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((((triple1) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
((((((triple2) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
((((((triple3) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
((((((((triple1) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule1 % int2)) ((((triple1) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is blue.
("Charlie" "is" "blue" "+")
int4
Gary is quiet.
("Gary" "is" "quiet" "+")
((((((((triple3) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is young.
("Gary" "is" "young" "+")
int4
Charlie is round.
("Charlie" "is" "round" "+")
((((((((triple1) -> (rule7 % int5))) -> (rule6 % int4))) -> (rule1 % int3)) ((((((((triple1) -> (rule7 % int5))) -> (rule6 % int4))) -> (rule1 % int3)) ((((triple1) -> (rule7 % int5))) -> (rule6 % int4))) -> (rule5 % int2))) -> (rule8 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
int4
Charlie is blue.
("Charlie" "is" "blue" "+")
int5