Bob is big. Charlie is furry. Erin is big. Gary is young. Young, furry things are smart. Blue things are not smart. If something is green then it is young. If something is rough and furry then it is not young. If something is young and green then it is big. Smart things are big. If something is young then it is not rough. If something is young then it is furry.
Bob is big.
("Bob" "is" "big" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Erin is big.
("Erin" "is" "big" "+")
Gary is young.
("Gary" "is" "young" "+")
Young, furry things are smart.
((("something" "is" "young" "+") ("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
Blue things are not smart.
((("something" "is" "blue" "+")) -> ("something" "is" "smart" "-"))
If something is green then it is young.
((("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
If something is rough and furry then it is not young.
((("something" "is" "rough" "+") ("something" "is" "furry" "+")) -> ("something" "is" "young" "-"))
If something is young and green then it is big.
((("something" "is" "young" "+") ("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
Smart things are big.
((("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
If something is young then it is not rough.
((("something" "is" "young" "+")) -> ("something" "is" "rough" "-"))
If something is young then it is furry.
((("something" "is" "young" "+")) -> ("something" "is" "furry" "+"))
Bob is big.
True
1
proof
[(triple1)]
("Bob" "is" "big" "+")
triple1
Erin is not big.
False
1
inv-proof
[(triple3)]
("Erin" "is" "big" "-")
triple3
Gary is not rough.
True
2
proof
[(((triple4) -> rule7))]
("Gary" "is" "rough" "-")
((triple4) -> (rule7 % int1))
Gary is not rough.
("Gary" "is" "rough" "-")
int1
Gary is rough.
False
2
inv-proof
[(((triple4) -> rule7))]
("Gary" "is" "rough" "+")
((triple4) -> (rule7 % int1))
Gary is not rough.
("Gary" "is" "rough" "-")
int1
Gary is smart.
True
4
proof
[(((triple4 ((triple4) -> rule8)) -> rule1))]
("Gary" "is" "smart" "+")
((triple4 ((triple4) -> (rule8 % int2))) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is not smart.
False
4
inv-proof
[(((triple4 ((triple4) -> rule8)) -> rule1))]
("Gary" "is" "smart" "-")
((triple4 ((triple4) -> (rule8 % int2))) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is big.
True
5
proof
[(((((triple4 ((triple4) -> rule8)) -> rule1)) -> rule6))]
("Gary" "is" "big" "+")
((((triple4 ((triple4) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is not big.
False
5
inv-proof
[(((((triple4 ((triple4) -> rule8)) -> rule1)) -> rule6))]
("Gary" "is" "big" "-")
((((triple4 ((triple4) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Charlie is not smart.
Unknown
inv-rconc
[@2: Charlie is smart.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Charlie" "is" "smart" "-")
Charlie is young.
Unknown
rconc
[@1: Charlie is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "young" "+")
Bob is not young.
Unknown
inv-rconc
[@1: Bob is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "young" "-")
Erin is young.
Unknown
rconc
[@1: Erin is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "young" "+")
Gary is not green.
Unknown
inv-random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "-")
Erin is rough.
Unknown
random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "+")
Charlie is not green.
Unknown
inv-random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
@0: Bob is big.[(triple1)] Charlie is furry.[(triple2)] Erin is big.[(triple3)] Gary is young.[(triple4)] @1: Gary is furry.[(((triple4) -> rule8))] Gary is not rough.[(((triple4) -> rule7))] @2: Gary is smart.[(((triple4 ((triple4) -> rule8)) -> rule1))] @3: Gary is big.[(((((triple4 ((triple4) -> rule8)) -> rule1)) -> rule6))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Erin is big.
("Erin" "is" "big" "+")
triple3
Gary is young.
("Gary" "is" "young" "+")
triple4
Gary is furry.
("Gary" "is" "furry" "+")
((triple4) -> (rule8 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is not rough.
("Gary" "is" "rough" "-")
((triple4) -> (rule7 % int1))
Gary is not rough.
("Gary" "is" "rough" "-")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((triple4 ((triple4) -> (rule8 % int2))) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
((((triple4 ((triple4) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3