Anne is red. Bob is young. Dave is rough. Gary is smart. Rough things are young. If Bob is young then Bob is furry. If Gary is red and Gary is smart then Gary is furry. If something is furry and rough then it is red. Red, kind things are young. If something is smart then it is furry. All young, rough things are smart. If something is smart then it is kind.
Anne is red.
("Anne" "is" "red" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Rough things are young.
((("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
If Bob is young then Bob is furry.
((("Bob" "is" "young" "+")) -> ("Bob" "is" "furry" "+"))
If Gary is red and Gary is smart then Gary is furry.
((("Gary" "is" "red" "+") ("Gary" "is" "smart" "+")) -> ("Gary" "is" "furry" "+"))
If something is furry and rough then it is red.
((("something" "is" "furry" "+") ("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
Red, kind things are young.
((("something" "is" "red" "+") ("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
If something is smart then it is furry.
((("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
All young, rough things are smart.
((("something" "is" "young" "+") ("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
If something is smart then it is kind.
((("something" "is" "smart" "+")) -> ("something" "is" "kind" "+"))
Bob is young.
True
1
proof
[(triple2)]
("Bob" "is" "young" "+")
triple2
Anne is not red.
False
1
inv-proof
[(triple1)]
("Anne" "is" "red" "-")
triple1
Bob is furry.
True
2
proof
[(((triple2) -> rule2))]
("Bob" "is" "furry" "+")
((triple2) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Dave is not young.
False
2
inv-proof
[(((triple3) -> rule1))]
("Dave" "is" "young" "-")
((triple3) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is smart.
True
4
proof
[(((((triple3) -> rule1) triple3) -> rule7))]
("Dave" "is" "smart" "+")
((((triple3) -> (rule1 % int2)) triple3) -> (rule7 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is not smart.
False
4
inv-proof
[(((((triple3) -> rule1) triple3) -> rule7))]
("Dave" "is" "smart" "-")
((((triple3) -> (rule1 % int2)) triple3) -> (rule7 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is furry.
True
5
proof
[(((((((triple3) -> rule1) triple3) -> rule7)) -> rule6))]
("Dave" "is" "furry" "+")
((((((triple3) -> (rule1 % int3)) triple3) -> (rule7 % int2))) -> (rule6 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is not furry.
False
5
inv-proof
[(((((((triple3) -> rule1) triple3) -> rule7)) -> rule6))]
("Dave" "is" "furry" "-")
((((((triple3) -> (rule1 % int3)) triple3) -> (rule7 % int2))) -> (rule6 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Gary is not red.
Unknown
inv-rconc
[@1: Gary is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "red" "-")
Bob is red.
Unknown
rconc
[@1: Bob is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "red" "+")
Anne is not young.
Unknown
inv-rconc
[@3: Anne is young.[CWA. Example of deepest failure = (rule5 <- rule8 <- rule7 <- FAIL)]]
("Anne" "is" "young" "-")
Anne is furry.
Unknown
rconc
[@2: Anne is furry.[CWA. Example of deepest failure = (rule6 <- rule7 <- FAIL)]]
("Anne" "is" "furry" "+")
Bob is not rough.
Unknown
inv-random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "-")
Anne is white.
Unknown
random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "+")
Bob is not white.
Unknown
inv-random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "-")
Gary is white.
Unknown
random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "+")
@0: Anne is red.[(triple1)] Bob is young.[(triple2)] Dave is rough.[(triple3)] Gary is smart.[(triple4)] @1: Bob is furry.[(((triple2) -> rule2))] Dave is young.[(((triple3) -> rule1))] Gary is furry.[(((triple4) -> rule6))] Gary is kind.[(((triple4) -> rule8))] @2: Dave is smart.[(((((triple3) -> rule1) triple3) -> rule7))] @3: Dave is furry.[(((((((triple3) -> rule1) triple3) -> rule7)) -> rule6))] Dave is kind.[(((((((triple3) -> rule1) triple3) -> rule7)) -> rule8))] @4: Dave is red.[(((((((((triple3) -> rule1) triple3) -> rule7)) -> rule6) triple3) -> rule4))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Bob is young.
("Bob" "is" "young" "+")
triple2
Dave is rough.
("Dave" "is" "rough" "+")
triple3
Gary is smart.
("Gary" "is" "smart" "+")
triple4
Bob is furry.
("Bob" "is" "furry" "+")
((triple2) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((triple3) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
((triple4) -> (rule6 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((triple4) -> (rule8 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((((triple3) -> (rule1 % int2)) triple3) -> (rule7 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
((((((triple3) -> (rule1 % int3)) triple3) -> (rule7 % int2))) -> (rule6 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
((((((triple3) -> (rule1 % int3)) triple3) -> (rule7 % int2))) -> (rule8 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
((((((((triple3) -> (rule1 % int4)) triple3) -> (rule7 % int3))) -> (rule6 % int2)) triple3) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4