Dave is blue. Fiona is quiet. Gary is nice. Smart things are furry. If something is rough then it is blue. If Gary is nice and Gary is quiet then Gary is rough. If something is nice then it is rough. Blue things are quiet. Quiet things are smart. If something is smart and blue then it is kind. If something is furry then it is kind.
Dave is blue.
("Dave" "is" "blue" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Smart things are furry.
((("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
If something is rough then it is blue.
((("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
If Gary is nice and Gary is quiet then Gary is rough.
((("Gary" "is" "nice" "+") ("Gary" "is" "quiet" "+")) -> ("Gary" "is" "rough" "+"))
If something is nice then it is rough.
((("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
Blue things are quiet.
((("something" "is" "blue" "+")) -> ("something" "is" "quiet" "+"))
Quiet things are smart.
((("something" "is" "quiet" "+")) -> ("something" "is" "smart" "+"))
If something is smart and blue then it is kind.
((("something" "is" "smart" "+") ("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
If something is furry then it is kind.
((("something" "is" "furry" "+")) -> ("something" "is" "kind" "+"))
Dave is blue.
True
1
proof
[(triple1)]
("Dave" "is" "blue" "+")
triple1
Gary is not nice.
False
1
inv-proof
[(triple3)]
("Gary" "is" "nice" "-")
triple3
Fiona is smart.
True
2
proof
[(((triple2) -> rule6))]
("Fiona" "is" "smart" "+")
((triple2) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is not smart.
False
2
inv-proof
[(((triple2) -> rule6))]
("Fiona" "is" "smart" "-")
((triple2) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is furry.
True
3
proof
[(((((triple2) -> rule6)) -> rule1))]
("Fiona" "is" "furry" "+")
((((triple2) -> (rule6 % int2))) -> (rule1 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Dave is not smart.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule6))]
("Dave" "is" "smart" "-")
((((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Fiona is kind.
True
4
proof
[(((((((triple2) -> rule6)) -> rule1)) -> rule8))]
("Fiona" "is" "kind" "+")
((((((triple2) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Dave is not kind.
False
5
inv-proof
[(((((((triple1) -> rule5)) -> rule6) triple1) -> rule7) OR ((((((((triple1) -> rule5)) -> rule6)) -> rule1)) -> rule8))]
("Dave" "is" "kind" "-")
((((((triple1) -> (rule5 % int3))) -> (rule6 % int2)) triple1) -> (rule7 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
((((((((triple1) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
int4
Fiona is not blue.
Unknown
inv-rconc
[@2: Fiona is blue.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("Fiona" "is" "blue" "-")
Dave is rough.
Unknown
rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "rough" "+")
Fiona is not rough.
Unknown
inv-rconc
[@1: Fiona is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "rough" "-")
Fiona is nice.
Unknown
random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "+")
@0: Dave is blue.[(triple1)] Fiona is quiet.[(triple2)] Gary is nice.[(triple3)] @1: Dave is quiet.[(((triple1) -> rule5))] Fiona is smart.[(((triple2) -> rule6))] Gary is rough.[(((triple3) -> rule4))] @2: Dave is smart.[(((((triple1) -> rule5)) -> rule6))] Fiona is furry.[(((((triple2) -> rule6)) -> rule1))] Gary is blue.[(((((triple3) -> rule4)) -> rule2))] @3: Dave is furry.[(((((((triple1) -> rule5)) -> rule6)) -> rule1))] Dave is kind.[(((((((triple1) -> rule5)) -> rule6) triple1) -> rule7) OR ((((((((triple1) -> rule5)) -> rule6)) -> rule1)) -> rule8))] Fiona is kind.[(((((((triple2) -> rule6)) -> rule1)) -> rule8))] Gary is quiet.[(((((((triple3) -> rule4)) -> rule2)) -> rule5))] @4: Gary is smart.[(((((((((triple3) -> rule4)) -> rule2)) -> rule5)) -> rule6))] @5: Gary is furry.[(((((((((((triple3) -> rule4)) -> rule2)) -> rule5)) -> rule6)) -> rule1))] Gary is kind.[(((((((((((triple3) -> rule4)) -> rule2)) -> rule5)) -> rule6) ((((triple3) -> rule4)) -> rule2)) -> rule7) OR ((((((((((((triple3) -> rule4)) -> rule2)) -> rule5)) -> rule6)) -> rule1)) -> rule8))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple2
Gary is nice.
("Gary" "is" "nice" "+")
triple3
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple1) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple2) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple3) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
((((triple2) -> (rule6 % int2))) -> (rule1 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
((((triple3) -> (rule4 % int2))) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
((((((triple1) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
((((((triple1) -> (rule5 % int3))) -> (rule6 % int2)) triple1) -> (rule7 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
((((((((triple1) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
int4
Fiona is kind.
("Fiona" "is" "kind" "+")
((((((triple2) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
((((((triple3) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
((((((((triple3) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
int4
Gary is furry.
("Gary" "is" "furry" "+")
((((((((((triple3) -> (rule4 % int5))) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
int4
Gary is rough.
("Gary" "is" "rough" "+")
int5
Gary is kind.
("Gary" "is" "kind" "+")
((((((((((triple3) -> (rule4 % int5))) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule6 % int2)) ((((triple3) -> (rule4 % int5))) -> (rule2 % int4))) -> (rule7 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
int4
Gary is rough.
("Gary" "is" "rough" "+")
int5
((((((((((((triple3) -> (rule4 % int6))) -> (rule2 % int5))) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
Gary is blue.
("Gary" "is" "blue" "+")
int5
Gary is rough.
("Gary" "is" "rough" "+")
int6