Bob is green. Bob is young. Dave is cold. Dave is rough. Erin is young. Gary is green. Gary is smart. All cold, green people are rough. All cold, rough people are young. Rough people are round. If Bob is smart then Bob is big. All green people are smart. All green, smart people are young. If someone is round then they are young. All big people are cold.
Bob is green.
("Bob" "is" "green" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is smart.
("Gary" "is" "smart" "+")
All cold, green people are rough.
((("someone" "is" "cold" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
All cold, rough people are young.
((("someone" "is" "cold" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "young" "+"))
Rough people are round.
((("someone" "is" "rough" "+")) -> ("someone" "is" "round" "+"))
If Bob is smart then Bob is big.
((("Bob" "is" "smart" "+")) -> ("Bob" "is" "big" "+"))
All green people are smart.
((("someone" "is" "green" "+")) -> ("someone" "is" "smart" "+"))
All green, smart people are young.
((("someone" "is" "green" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "young" "+"))
If someone is round then they are young.
((("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
All big people are cold.
((("someone" "is" "big" "+")) -> ("someone" "is" "cold" "+"))
Bob is young.
True
1
proof
[(triple2 OR ((triple1 ((triple1) -> rule5)) -> rule6) OR ((((((((triple1) -> rule5)) -> rule4)) -> rule8) ((((((((triple1) -> rule5)) -> rule4)) -> rule8) triple1) -> rule1)) -> rule2) OR ((((((((((((triple1) -> rule5)) -> rule4)) -> rule8) triple1) -> rule1)) -> rule3)) -> rule7))]
("Bob" "is" "young" "+")
triple2
((triple1 ((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
((((((((triple1) -> (rule5 % int5))) -> (rule4 % int4))) -> (rule8 % int3)) ((((((((triple1) -> (rule5 % int5))) -> (rule4 % int4))) -> (rule8 % int3)) triple1) -> (rule1 % int2))) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
int4
Bob is smart.
("Bob" "is" "smart" "+")
int5
((((((((((((triple1) -> (rule5 % int6))) -> (rule4 % int5))) -> (rule8 % int4)) triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
int4
Bob is big.
("Bob" "is" "big" "+")
int5
Bob is smart.
("Bob" "is" "smart" "+")
int6
Gary is not smart.
False
1
inv-proof
[(triple7 OR ((triple6) -> rule5))]
("Gary" "is" "smart" "-")
triple7
((triple6) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is young.
True
3
proof
[(((triple6 triple7) -> rule6) OR ((triple6 ((triple6) -> rule5)) -> rule6))]
("Gary" "is" "young" "+")
((triple6 triple7) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
((triple6 ((triple6) -> (rule5 % int2))) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Bob is not smart.
False
2
inv-proof
[(((triple1) -> rule5))]
("Bob" "is" "smart" "-")
((triple1) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is big.
True
3
proof
[(((((triple1) -> rule5)) -> rule4))]
("Bob" "is" "big" "+")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is not big.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule4))]
("Bob" "is" "big" "-")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is cold.
True
4
proof
[(((((((triple1) -> rule5)) -> rule4)) -> rule8))]
("Bob" "is" "cold" "+")
((((((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is not cold.
False
4
inv-proof
[(((((((triple1) -> rule5)) -> rule4)) -> rule8))]
("Bob" "is" "cold" "-")
((((((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is rough.
True
6
proof
[(((((((((triple1) -> rule5)) -> rule4)) -> rule8) triple1) -> rule1))]
("Bob" "is" "rough" "+")
((((((((triple1) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule8 % int2)) triple1) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
Bob is not rough.
False
6
inv-proof
[(((((((((triple1) -> rule5)) -> rule4)) -> rule8) triple1) -> rule1))]
("Bob" "is" "rough" "-")
((((((((triple1) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule8 % int2)) triple1) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
Bob is round.
True
7
proof
[(((((((((((triple1) -> rule5)) -> rule4)) -> rule8) triple1) -> rule1)) -> rule3))]
("Bob" "is" "round" "+")
((((((((((triple1) -> (rule5 % int5))) -> (rule4 % int4))) -> (rule8 % int3)) triple1) -> (rule1 % int2))) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
int4
Bob is smart.
("Bob" "is" "smart" "+")
int5
Bob is not round.
False
7
inv-proof
[(((((((((((triple1) -> rule5)) -> rule4)) -> rule8) triple1) -> rule1)) -> rule3))]
("Bob" "is" "round" "-")
((((((((((triple1) -> (rule5 % int5))) -> (rule4 % int4))) -> (rule8 % int3)) triple1) -> (rule1 % int2))) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
int4
Bob is smart.
("Bob" "is" "smart" "+")
int5
Erin is not round.
Unknown
inv-rconc
[@2: Erin is round.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Erin" "is" "round" "-")
Erin is smart.
Unknown
rconc
[@1: Erin is smart.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "smart" "+")
Erin is not rough.
Unknown
inv-rconc
[@1: Erin is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "rough" "-")
Dave is smart.
Unknown
rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "smart" "+")
Gary is not round.
Unknown
inv-rconc
[@3: Gary is round.[CWA. Example of deepest failure = (rule3 <- rule1 <- rule8 <- FAIL)]]
("Gary" "is" "round" "-")
Gary is rough.
Unknown
rconc
[@2: Gary is rough.[CWA. Example of deepest failure = (rule1 <- rule8 <- FAIL)]]
("Gary" "is" "rough" "+")
Gary is not big.
Unknown
inv-random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
Erin is not green.
Unknown
inv-random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
@0: Bob is green.[(triple1)] Bob is young.[(triple2 OR ((triple1 ((triple1) -> rule5)) -> rule6) OR ((((((((triple1) -> rule5)) -> rule4)) -> rule8) ((((((((triple1) -> rule5)) -> rule4)) -> rule8) triple1) -> rule1)) -> rule2) OR ((((((((((((triple1) -> rule5)) -> rule4)) -> rule8) triple1) -> rule1)) -> rule3)) -> rule7))] Dave is cold.[(triple3)] Dave is rough.[(triple4)] Erin is young.[(triple5)] Gary is green.[(triple6)] Gary is smart.[(triple7 OR ((triple6) -> rule5))] @1: Bob is smart.[(((triple1) -> rule5))] Dave is round.[(((triple4) -> rule3))] Dave is young.[(((triple3 triple4) -> rule2) OR ((((triple4) -> rule3)) -> rule7))] Gary is young.[(((triple6 triple7) -> rule6) OR ((triple6 ((triple6) -> rule5)) -> rule6))] @2: Bob is big.[(((((triple1) -> rule5)) -> rule4))] @3: Bob is cold.[(((((((triple1) -> rule5)) -> rule4)) -> rule8))] @4: Bob is rough.[(((((((((triple1) -> rule5)) -> rule4)) -> rule8) triple1) -> rule1))] @5: Bob is round.[(((((((((((triple1) -> rule5)) -> rule4)) -> rule8) triple1) -> rule1)) -> rule3))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Bob is young.
("Bob" "is" "young" "+")
triple2
((triple1 ((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
((((((((triple1) -> (rule5 % int5))) -> (rule4 % int4))) -> (rule8 % int3)) ((((((((triple1) -> (rule5 % int5))) -> (rule4 % int4))) -> (rule8 % int3)) triple1) -> (rule1 % int2))) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
int4
Bob is smart.
("Bob" "is" "smart" "+")
int5
((((((((((((triple1) -> (rule5 % int6))) -> (rule4 % int5))) -> (rule8 % int4)) triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
int4
Bob is big.
("Bob" "is" "big" "+")
int5
Bob is smart.
("Bob" "is" "smart" "+")
int6
Dave is cold.
("Dave" "is" "cold" "+")
triple3
Dave is rough.
("Dave" "is" "rough" "+")
triple4
Erin is young.
("Erin" "is" "young" "+")
triple5
Gary is green.
("Gary" "is" "green" "+")
triple6
Gary is smart.
("Gary" "is" "smart" "+")
triple7
((triple6) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((triple1) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((triple4) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((triple3 triple4) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((((triple4) -> (rule3 % int2))) -> (rule7 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
((triple6 triple7) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
((triple6 ((triple6) -> (rule5 % int2))) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
((((((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
((((((((triple1) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule8 % int2)) triple1) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
Bob is round.
("Bob" "is" "round" "+")
((((((((((triple1) -> (rule5 % int5))) -> (rule4 % int4))) -> (rule8 % int3)) triple1) -> (rule1 % int2))) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
int4
Bob is smart.
("Bob" "is" "smart" "+")
int5