Bob is smart. Erin is red. Gary is red. Harry is furry. If something is smart and not round then it is red. If something is smart then it is red. If something is red then it is furry. Furry things are young. Round things are not young. Green, smart things are young. If something is furry and round then it is big. If Harry is young then Harry is red.
Bob is smart.
("Bob" "is" "smart" "+")
Erin is red.
("Erin" "is" "red" "+")
Gary is red.
("Gary" "is" "red" "+")
Harry is furry.
("Harry" "is" "furry" "+")
If something is smart and not round then it is red.
((("something" "is" "smart" "+") ("something" "is" "round" "~")) -> ("something" "is" "red" "+"))
If something is smart then it is red.
((("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
If something is red then it is furry.
((("something" "is" "red" "+")) -> ("something" "is" "furry" "+"))
Furry things are young.
((("something" "is" "furry" "+")) -> ("something" "is" "young" "+"))
Round things are not young.
((("something" "is" "round" "+")) -> ("something" "is" "young" "-"))
Green, smart things are young.
((("something" "is" "green" "+") ("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
If something is furry and round then it is big.
((("something" "is" "furry" "+") ("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
If Harry is young then Harry is red.
((("Harry" "is" "young" "+")) -> ("Harry" "is" "red" "+"))
Harry is furry.
True
1
proof
[(triple4)]
("Harry" "is" "furry" "+")
triple4
Erin is not red.
False
1
inv-proof
[(triple2)]
("Erin" "is" "red" "-")
triple2
Bob is red.
True
2
proof
[(((triple1) -> rule2))]
("Bob" "is" "red" "+")
((triple1) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Erin is not furry.
False
2
inv-proof
[(((triple2) -> rule3))]
("Erin" "is" "furry" "-")
((triple2) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Bob is furry.
True
3
proof
[(((((triple1) -> rule2)) -> rule3))]
("Bob" "is" "furry" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Harry is not red.
False
3
inv-proof
[(((((triple4) -> rule4)) -> rule8))]
("Harry" "is" "red" "-")
((((triple4) -> (rule4 % int2))) -> (rule8 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Bob is young.
True
4
proof
[(((((((triple1) -> rule2)) -> rule3)) -> rule4))]
("Bob" "is" "young" "+")
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is not young.
False
4
inv-proof
[(((((((triple1) -> rule2)) -> rule3)) -> rule4))]
("Bob" "is" "young" "-")
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Gary is not big.
Unknown
inv-rconc
[@1: Gary is big.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Gary" "is" "big" "-")
Harry is big.
Unknown
rconc
[@1: Harry is big.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Harry" "is" "big" "+")
Erin is not big.
Unknown
inv-rconc
[@1: Erin is big.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Erin" "is" "big" "-")
Bob is big.
Unknown
rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Bob" "is" "big" "+")
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
Erin is not round.
Unknown
inv-random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
@0: Bob is smart.[(triple1)] Erin is red.[(triple2)] Gary is red.[(triple3)] Harry is furry.[(triple4)] @1: Bob is red.[(((triple1) -> rule2))] Erin is furry.[(((triple2) -> rule3))] Gary is furry.[(((triple3) -> rule3))] Harry is young.[(((triple4) -> rule4))] @2: Bob is furry.[(((((triple1) -> rule2)) -> rule3))] Erin is young.[(((((triple2) -> rule3)) -> rule4))] Gary is young.[(((((triple3) -> rule3)) -> rule4))] Harry is red.[(((((triple4) -> rule4)) -> rule8))] @3: Bob is young.[(((((((triple1) -> rule2)) -> rule3)) -> rule4))]
Bob is smart.
("Bob" "is" "smart" "+")
triple1
Erin is red.
("Erin" "is" "red" "+")
triple2
Gary is red.
("Gary" "is" "red" "+")
triple3
Harry is furry.
("Harry" "is" "furry" "+")
triple4
Bob is red.
("Bob" "is" "red" "+")
((triple1) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((triple2) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
((triple3) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple4) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
((((triple3) -> (rule3 % int2))) -> (rule4 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
((((triple4) -> (rule4 % int2))) -> (rule8 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3