Charlie is green. Dave is big. Gary is not smart. All big things are smart. If Dave is big and Dave is smart then Dave is young. If something is big and not smart then it is not young. Rough things are young. Quiet things are green. Big, blue things are green. All young things are blue. If something is quiet then it is blue.
Charlie is green.
("Charlie" "is" "green" "+")
Dave is big.
("Dave" "is" "big" "+")
Gary is not smart.
("Gary" "is" "smart" "-")
All big things are smart.
((("something" "is" "big" "+")) -> ("something" "is" "smart" "+"))
If Dave is big and Dave is smart then Dave is young.
((("Dave" "is" "big" "+") ("Dave" "is" "smart" "+")) -> ("Dave" "is" "young" "+"))
If something is big and not smart then it is not young.
((("something" "is" "big" "+") ("something" "is" "smart" "~")) -> ("something" "is" "young" "-"))
Rough things are young.
((("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
Quiet things are green.
((("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
Big, blue things are green.
((("something" "is" "big" "+") ("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
All young things are blue.
((("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
If something is quiet then it is blue.
((("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
Dave is big.
True
1
proof
[(triple2)]
("Dave" "is" "big" "+")
triple2
Dave is not big.
False
1
inv-proof
[(triple2)]
("Dave" "is" "big" "-")
triple2
Dave is smart.
True
2
proof
[(((triple2) -> rule1))]
("Dave" "is" "smart" "+")
((triple2) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is not smart.
False
2
inv-proof
[(((triple2) -> rule1))]
("Dave" "is" "smart" "-")
((triple2) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is young.
True
4
proof
[(((triple2 ((triple2) -> rule1)) -> rule2))]
("Dave" "is" "young" "+")
((triple2 ((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is not young.
False
4
inv-proof
[(((triple2 ((triple2) -> rule1)) -> rule2))]
("Dave" "is" "young" "-")
((triple2 ((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is blue.
True
5
proof
[(((((triple2 ((triple2) -> rule1)) -> rule2)) -> rule7))]
("Dave" "is" "blue" "+")
((((triple2 ((triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is not blue.
False
5
inv-proof
[(((((triple2 ((triple2) -> rule1)) -> rule2)) -> rule7))]
("Dave" "is" "blue" "-")
((((triple2 ((triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Gary is not green.
Unknown
inv-rconc
[@1: Gary is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "green" "-")
Charlie is young.
Unknown
rconc
[@1: Charlie is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "young" "+")
Gary is not blue.
Unknown
inv-rconc
[@2: Gary is blue.[CWA. Example of deepest failure = (rule7 <- rule4 <- FAIL)]]
("Gary" "is" "blue" "-")
Gary is young.
Unknown
rconc
[@1: Gary is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "young" "+")
Dave is not rough.
Unknown
inv-random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
@0: Charlie is green.[(triple1)] Dave is big.[(triple2)] Gary is not smart.[(triple3)] @1: Dave is smart.[(((triple2) -> rule1))] @2: Dave is young.[(((triple2 ((triple2) -> rule1)) -> rule2))] @3: Dave is blue.[(((((triple2 ((triple2) -> rule1)) -> rule2)) -> rule7))] @4: Dave is green.[(((triple2 ((((triple2 ((triple2) -> rule1)) -> rule2)) -> rule7)) -> rule6))]
Charlie is green.
("Charlie" "is" "green" "+")
triple1
Dave is big.
("Dave" "is" "big" "+")
triple2
Gary is not smart.
("Gary" "is" "smart" "-")
triple3
Dave is smart.
("Dave" "is" "smart" "+")
((triple2) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((triple2 ((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
((((triple2 ((triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
((triple2 ((((triple2 ((triple2) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
int4