Bob is blue. Bob is cold. Bob is rough. Dave is rough. Erin is blue. Erin is rough. Erin is young. Gary is rough. Gary is round. Gary is young. All rough, smart things are blue. All blue, smart things are green. If something is young then it is smart.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is young.
("Gary" "is" "young" "+")
All rough, smart things are blue.
((("something" "is" "rough" "+") ("something" "is" "smart" "+")) -> ("something" "is" "blue" "+"))
All blue, smart things are green.
((("something" "is" "blue" "+") ("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
If something is young then it is smart.
((("something" "is" "young" "+")) -> ("something" "is" "smart" "+"))
Dave is rough.
True
1
proof
[(triple4)]
("Dave" "is" "rough" "+")
triple4
Dave is not rough.
False
1
inv-proof
[(triple4)]
("Dave" "is" "rough" "-")
triple4
Gary is smart.
True
2
proof
[(((triple10) -> rule3))]
("Gary" "is" "smart" "+")
((triple10) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is not smart.
False
2
inv-proof
[(((triple10) -> rule3))]
("Gary" "is" "smart" "-")
((triple10) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Erin is green.
True
4
proof
[(((triple5 ((triple7) -> rule3)) -> rule2) OR ((((triple6 ((triple7) -> rule3)) -> rule1) ((triple7) -> rule3)) -> rule2))]
("Erin" "is" "green" "+")
((triple5 ((triple7) -> (rule3 % int2))) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((triple6 ((triple7) -> (rule3 % int3))) -> (rule1 % int2)) ((triple7) -> (rule3 % int3))) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Gary is not blue.
False
4
inv-proof
[(((triple8 ((triple10) -> rule3)) -> rule1))]
("Gary" "is" "blue" "-")
((triple8 ((triple10) -> (rule3 % int2))) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is green.
True
7
proof
[(((((triple8 ((triple10) -> rule3)) -> rule1) ((triple10) -> rule3)) -> rule2))]
("Gary" "is" "green" "+")
((((triple8 ((triple10) -> (rule3 % int3))) -> (rule1 % int2)) ((triple10) -> (rule3 % int3))) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is not green.
False
7
inv-proof
[(((((triple8 ((triple10) -> rule3)) -> rule1) ((triple10) -> rule3)) -> rule2))]
("Gary" "is" "green" "-")
((((triple8 ((triple10) -> (rule3 % int3))) -> (rule1 % int2)) ((triple10) -> (rule3 % int3))) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Bob is not smart.
Unknown
inv-rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "smart" "-")
Dave is smart.
Unknown
rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "smart" "+")
Bob is not green.
Unknown
inv-rconc
[@2: Bob is green.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Bob" "is" "green" "-")
Dave is green.
Unknown
rconc
[@2: Dave is green.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Dave" "is" "green" "+")
Dave is not round.
Unknown
inv-random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
Dave is not cold.
Unknown
inv-random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
@0: Bob is blue.[(triple1)] Bob is cold.[(triple2)] Bob is rough.[(triple3)] Dave is rough.[(triple4)] Erin is blue.[(triple5 OR ((triple6 ((triple7) -> rule3)) -> rule1))] Erin is rough.[(triple6)] Erin is young.[(triple7)] Gary is rough.[(triple8)] Gary is round.[(triple9)] Gary is young.[(triple10)] @1: Erin is smart.[(((triple7) -> rule3))] Gary is smart.[(((triple10) -> rule3))] @2: Erin is green.[(((triple5 ((triple7) -> rule3)) -> rule2) OR ((((triple6 ((triple7) -> rule3)) -> rule1) ((triple7) -> rule3)) -> rule2))] Gary is blue.[(((triple8 ((triple10) -> rule3)) -> rule1))] @3: Gary is green.[(((((triple8 ((triple10) -> rule3)) -> rule1) ((triple10) -> rule3)) -> rule2))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is rough.
("Bob" "is" "rough" "+")
triple3
Dave is rough.
("Dave" "is" "rough" "+")
triple4
Erin is blue.
("Erin" "is" "blue" "+")
triple5
((triple6 ((triple7) -> (rule3 % int2))) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
triple6
Erin is young.
("Erin" "is" "young" "+")
triple7
Gary is rough.
("Gary" "is" "rough" "+")
triple8
Gary is round.
("Gary" "is" "round" "+")
triple9
Gary is young.
("Gary" "is" "young" "+")
triple10
Erin is smart.
("Erin" "is" "smart" "+")
((triple7) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((triple10) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
((triple5 ((triple7) -> (rule3 % int2))) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((triple6 ((triple7) -> (rule3 % int3))) -> (rule1 % int2)) ((triple7) -> (rule3 % int3))) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
((triple8 ((triple10) -> (rule3 % int2))) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
((((triple8 ((triple10) -> (rule3 % int3))) -> (rule1 % int2)) ((triple10) -> (rule3 % int3))) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3