Erin is nice. Erin is red. Fiona is nice. Fiona is red. Fiona is rough. Fiona is young. Gary is rough. Gary is smart. Harry is red. Harry is rough. Harry is round. Young, red people are blue. If someone is red and young then they are rough. Rough people are smart. Young, smart people are nice. Round, nice people are rough. All smart people are round. Nice people are smart. If Fiona is round then Fiona is smart. All rough, nice people are young.
Erin is nice.
("Erin" "is" "nice" "+")
Erin is red.
("Erin" "is" "red" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
Young, red people are blue.
((("someone" "is" "young" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
If someone is red and young then they are rough.
((("someone" "is" "red" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
Rough people are smart.
((("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
Young, smart people are nice.
((("someone" "is" "young" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
Round, nice people are rough.
((("someone" "is" "round" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
All smart people are round.
((("someone" "is" "smart" "+")) -> ("someone" "is" "round" "+"))
Nice people are smart.
((("someone" "is" "nice" "+")) -> ("someone" "is" "smart" "+"))
If Fiona is round then Fiona is smart.
((("Fiona" "is" "round" "+")) -> ("Fiona" "is" "smart" "+"))
All rough, nice people are young.
((("someone" "is" "rough" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "young" "+"))
Fiona is rough.
True
1
proof
[(triple5 OR ((triple4 triple6) -> rule2) OR ((((((triple3) -> rule7)) -> rule6) triple3) -> rule5))]
("Fiona" "is" "rough" "+")
triple5
((triple4 triple6) -> (rule2 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
((((((triple3) -> (rule7 % int3))) -> (rule6 % int2)) triple3) -> (rule5 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is not young.
False
1
inv-proof
[(triple6 OR ((triple5 triple3) -> rule9) OR ((((((((triple3) -> rule7)) -> rule6) triple3) -> rule5) triple3) -> rule9))]
("Fiona" "is" "young" "-")
triple6
((triple5 triple3) -> (rule9 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
((((((((triple3) -> (rule7 % int4))) -> (rule6 % int3)) triple3) -> (rule5 % int2)) triple3) -> (rule9 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
int4
Fiona is smart.
True
2
proof
[(((triple3) -> rule7) OR ((triple5) -> rule3) OR ((((triple4 triple6) -> rule2)) -> rule3))]
("Fiona" "is" "smart" "+")
((triple3) -> (rule7 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((triple5) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((((triple4 triple6) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Gary is not round.
False
2
inv-proof
[(((triple8) -> rule6) OR ((((triple7) -> rule3)) -> rule6))]
("Gary" "is" "round" "-")
((triple8) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((((triple7) -> (rule3 % int2))) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Erin is round.
True
3
proof
[(((((triple1) -> rule7)) -> rule6))]
("Erin" "is" "round" "+")
((((triple1) -> (rule7 % int2))) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is not round.
False
3
inv-proof
[(((((triple1) -> rule7)) -> rule6))]
("Erin" "is" "round" "-")
((((triple1) -> (rule7 % int2))) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is rough.
True
5
proof
[(((((((triple1) -> rule7)) -> rule6) triple1) -> rule5))]
("Erin" "is" "rough" "+")
((((((triple1) -> (rule7 % int3))) -> (rule6 % int2)) triple1) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is not rough.
False
5
inv-proof
[(((((((triple1) -> rule7)) -> rule6) triple1) -> rule5))]
("Erin" "is" "rough" "-")
((((((triple1) -> (rule7 % int3))) -> (rule6 % int2)) triple1) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is young.
True
7
proof
[(((((((((triple1) -> rule7)) -> rule6) triple1) -> rule5) triple1) -> rule9))]
("Erin" "is" "young" "+")
((((((((triple1) -> (rule7 % int4))) -> (rule6 % int3)) triple1) -> (rule5 % int2)) triple1) -> (rule9 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
Erin is not young.
False
7
inv-proof
[(((((((((triple1) -> rule7)) -> rule6) triple1) -> rule5) triple1) -> rule9))]
("Erin" "is" "young" "-")
((((((((triple1) -> (rule7 % int4))) -> (rule6 % int3)) triple1) -> (rule5 % int2)) triple1) -> (rule9 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
Erin is blue.
True
9
proof
[(((((((((((triple1) -> rule7)) -> rule6) triple1) -> rule5) triple1) -> rule9) triple2) -> rule1))]
("Erin" "is" "blue" "+")
((((((((((triple1) -> (rule7 % int5))) -> (rule6 % int4)) triple1) -> (rule5 % int3)) triple1) -> (rule9 % int2)) triple2) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
int4
Erin is smart.
("Erin" "is" "smart" "+")
int5
Erin is not blue.
False
9
inv-proof
[(((((((((((triple1) -> rule7)) -> rule6) triple1) -> rule5) triple1) -> rule9) triple2) -> rule1))]
("Erin" "is" "blue" "-")
((((((((((triple1) -> (rule7 % int5))) -> (rule6 % int4)) triple1) -> (rule5 % int3)) triple1) -> (rule9 % int2)) triple2) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
int4
Erin is smart.
("Erin" "is" "smart" "+")
int5
Harry is not blue.
Unknown
inv-rconc
[@3: Harry is blue.[CWA. Example of deepest failure = (rule1 <- rule9 <- rule4 <- FAIL)]]
("Harry" "is" "blue" "-")
Gary is young.
Unknown
rconc
[@2: Gary is young.[CWA. Example of deepest failure = (rule9 <- rule4 <- FAIL)]]
("Gary" "is" "young" "+")
Harry is not nice.
Unknown
inv-rconc
[@2: Harry is nice.[CWA. Example of deepest failure = (rule4 <- rule9 <- FAIL)]]
("Harry" "is" "nice" "-")
Gary is nice.
Unknown
rconc
[@2: Gary is nice.[CWA. Example of deepest failure = (rule4 <- rule9 <- FAIL)]]
("Gary" "is" "nice" "+")
Gary is not blue.
Unknown
inv-rconc
[@1: Gary is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "blue" "-")
Harry is young.
Unknown
rconc
[@2: Harry is young.[CWA. Example of deepest failure = (rule9 <- rule4 <- FAIL)]]
("Harry" "is" "young" "+")
@0: Erin is nice.[(triple1)] Erin is red.[(triple2)] Fiona is nice.[(triple3 OR ((triple6 ((triple5) -> rule3)) -> rule4) OR ((triple6 ((((triple4 triple6) -> rule2)) -> rule3)) -> rule4))] Fiona is red.[(triple4)] Fiona is rough.[(triple5 OR ((triple4 triple6) -> rule2) OR ((((((triple3) -> rule7)) -> rule6) triple3) -> rule5))] Fiona is young.[(triple6 OR ((triple5 triple3) -> rule9) OR ((((((((triple3) -> rule7)) -> rule6) triple3) -> rule5) triple3) -> rule9))] Gary is rough.[(triple7)] Gary is smart.[(triple8 OR ((triple7) -> rule3))] Harry is red.[(triple9)] Harry is rough.[(triple10)] Harry is round.[(triple11 OR ((((triple10) -> rule3)) -> rule6))] @1: Erin is smart.[(((triple1) -> rule7))] Fiona is blue.[(((triple6 triple4) -> rule1) OR ((((triple5 triple3) -> rule9) triple4) -> rule1) OR ((((((((((triple3) -> rule7)) -> rule6) triple3) -> rule5) triple3) -> rule9) triple4) -> rule1))] Fiona is smart.[(((triple3) -> rule7) OR ((triple5) -> rule3) OR ((((triple4 triple6) -> rule2)) -> rule3))] Gary is round.[(((triple8) -> rule6) OR ((((triple7) -> rule3)) -> rule6))] Harry is smart.[(((triple10) -> rule3))] @2: Erin is round.[(((((triple1) -> rule7)) -> rule6))] Fiona is round.[(((((triple3) -> rule7)) -> rule6) OR ((((triple5) -> rule3)) -> rule6) OR ((((((triple4 triple6) -> rule2)) -> rule3)) -> rule6))] @3: Erin is rough.[(((((((triple1) -> rule7)) -> rule6) triple1) -> rule5))] @4: Erin is young.[(((((((((triple1) -> rule7)) -> rule6) triple1) -> rule5) triple1) -> rule9))] @5: Erin is blue.[(((((((((((triple1) -> rule7)) -> rule6) triple1) -> rule5) triple1) -> rule9) triple2) -> rule1))]
Erin is nice.
("Erin" "is" "nice" "+")
triple1
Erin is red.
("Erin" "is" "red" "+")
triple2
Fiona is nice.
("Fiona" "is" "nice" "+")
triple3
((triple6 ((triple5) -> (rule3 % int2))) -> (rule4 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((triple6 ((((triple4 triple6) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
triple4
Fiona is rough.
("Fiona" "is" "rough" "+")
triple5
((triple4 triple6) -> (rule2 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
((((((triple3) -> (rule7 % int3))) -> (rule6 % int2)) triple3) -> (rule5 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is young.
("Fiona" "is" "young" "+")
triple6
((triple5 triple3) -> (rule9 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
((((((((triple3) -> (rule7 % int4))) -> (rule6 % int3)) triple3) -> (rule5 % int2)) triple3) -> (rule9 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
int4
Gary is rough.
("Gary" "is" "rough" "+")
triple7
Gary is smart.
("Gary" "is" "smart" "+")
triple8
((triple7) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
triple9
Harry is rough.
("Harry" "is" "rough" "+")
triple10
Harry is round.
("Harry" "is" "round" "+")
triple11
((((triple10) -> (rule3 % int2))) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
((triple1) -> (rule7 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
((triple6 triple4) -> (rule1 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
((((triple5 triple3) -> (rule9 % int2)) triple4) -> (rule1 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
((((((((((triple3) -> (rule7 % int5))) -> (rule6 % int4)) triple3) -> (rule5 % int3)) triple3) -> (rule9 % int2)) triple4) -> (rule1 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Fiona is round.
("Fiona" "is" "round" "+")
int4
Fiona is smart.
("Fiona" "is" "smart" "+")
int5
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple3) -> (rule7 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((triple5) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((((triple4 triple6) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
((triple8) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((((triple7) -> (rule3 % int2))) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
((triple10) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
((((triple1) -> (rule7 % int2))) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
((((triple3) -> (rule7 % int2))) -> (rule6 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((((triple5) -> (rule3 % int2))) -> (rule6 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((((((triple4 triple6) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
((((((triple1) -> (rule7 % int3))) -> (rule6 % int2)) triple1) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
((((((((triple1) -> (rule7 % int4))) -> (rule6 % int3)) triple1) -> (rule5 % int2)) triple1) -> (rule9 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
Erin is blue.
("Erin" "is" "blue" "+")
((((((((((triple1) -> (rule7 % int5))) -> (rule6 % int4)) triple1) -> (rule5 % int3)) triple1) -> (rule9 % int2)) triple2) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
int4
Erin is smart.
("Erin" "is" "smart" "+")
int5