Bob is red. Gary is round. If Bob is young then Bob is big. Smart things are kind. All young, round things are smart. Kind, round things are blue. Blue, young things are kind. All big, kind things are round. If something is round then it is smart. All smart, blue things are red.
Bob is red.
("Bob" "is" "red" "+")
Gary is round.
("Gary" "is" "round" "+")
If Bob is young then Bob is big.
((("Bob" "is" "young" "+")) -> ("Bob" "is" "big" "+"))
Smart things are kind.
((("something" "is" "smart" "+")) -> ("something" "is" "kind" "+"))
All young, round things are smart.
((("something" "is" "young" "+") ("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
Kind, round things are blue.
((("something" "is" "kind" "+") ("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
Blue, young things are kind.
((("something" "is" "blue" "+") ("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
All big, kind things are round.
((("something" "is" "big" "+") ("something" "is" "kind" "+")) -> ("something" "is" "round" "+"))
If something is round then it is smart.
((("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
All smart, blue things are red.
((("something" "is" "smart" "+") ("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
Gary is round.
True
1
proof
[(triple2)]
("Gary" "is" "round" "+")
triple2
Gary is not round.
False
1
inv-proof
[(triple2)]
("Gary" "is" "round" "-")
triple2
Gary is smart.
True
2
proof
[(((triple2) -> rule7))]
("Gary" "is" "smart" "+")
((triple2) -> (rule7 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is not smart.
False
2
inv-proof
[(((triple2) -> rule7))]
("Gary" "is" "smart" "-")
((triple2) -> (rule7 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is kind.
True
3
proof
[(((((triple2) -> rule7)) -> rule2))]
("Gary" "is" "kind" "+")
((((triple2) -> (rule7 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is not kind.
False
3
inv-proof
[(((((triple2) -> rule7)) -> rule2))]
("Gary" "is" "kind" "-")
((((triple2) -> (rule7 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is blue.
True
5
proof
[(((((((triple2) -> rule7)) -> rule2) triple2) -> rule4))]
("Gary" "is" "blue" "+")
((((((triple2) -> (rule7 % int3))) -> (rule2 % int2)) triple2) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is not blue.
False
5
inv-proof
[(((((((triple2) -> rule7)) -> rule2) triple2) -> rule4))]
("Gary" "is" "blue" "-")
((((((triple2) -> (rule7 % int3))) -> (rule2 % int2)) triple2) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Bob is not round.
Unknown
inv-rconc
[@2: Bob is round.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Bob" "is" "round" "-")
Bob is kind.
Unknown
rconc
[@4: Bob is kind.[CWA. Example of deepest failure = (rule2 <- rule7 <- rule6 <- rule1 <- FAIL)]]
("Bob" "is" "kind" "+")
Bob is not smart.
Unknown
inv-rconc
[@3: Bob is smart.[CWA. Example of deepest failure = (rule7 <- rule6 <- rule1 <- FAIL)]]
("Bob" "is" "smart" "-")
Bob is big.
Unknown
rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "big" "+")
Gary is not big.
Unknown
inv-random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
@0: Bob is red.[(triple1)] Gary is round.[(triple2)] @1: Gary is smart.[(((triple2) -> rule7))] @2: Gary is kind.[(((((triple2) -> rule7)) -> rule2))] @3: Gary is blue.[(((((((triple2) -> rule7)) -> rule2) triple2) -> rule4))] @4: Gary is red.[(((((triple2) -> rule7) ((((((triple2) -> rule7)) -> rule2) triple2) -> rule4)) -> rule8))]
Bob is red.
("Bob" "is" "red" "+")
triple1
Gary is round.
("Gary" "is" "round" "+")
triple2
Gary is smart.
("Gary" "is" "smart" "+")
((triple2) -> (rule7 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((((triple2) -> (rule7 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
((((((triple2) -> (rule7 % int3))) -> (rule2 % int2)) triple2) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
((((triple2) -> (rule7 % int4)) ((((((triple2) -> (rule7 % int4))) -> (rule2 % int3)) triple2) -> (rule4 % int2))) -> (rule8 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4